Theorem coeq2d 5865

Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
coeq2d	⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Proof of Theorem coeq2d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		coeq2 5861	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   = wceq 1534   ∘ ccom 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964  df-br 5149  df-opab 5211  df-co 5687

This theorem is referenced by:  coeq12d  5867  dfpo2  6300  f1ococnv1  6868  funcoeqres  6870  fcof1oinvd  7302  foeqcnvco  7309  f1ofvswap  7315  fparlem3  8119  fparlem4  8120  offsplitfpar  8124  csbwrecsg  8327  mapen  9166  mapfien  9432  wemapwe  9721  hashfacen  14446  hashfacenOLD  14447  s1co  14817  pfxco  14822  relexpsucnnl  15010  relexpsucl  15011  relexpsucld  15014  relexpcnv  15015  relexpaddnn  15031  relexpaddg  15033  prdsval  17437  isofval  17740  cofuass  17875  cofurid  17877  fucid  17963  setcinv  18079  catcisolem  18099  curf2ndf  18239  pwsco2mhm  18785  symggrplem  18836  smndex1igid  18856  f1omvdco2  19403  psgnunilem1  19448  efginvrel2  19682  efginvrel1  19683  vrgpinv  19724  frgpuplem  19727  gsumval3  19862  gsumzf1o  19867  psrass1lemOLD  21874  psrass1lem  21877  mpfrcl  22031  evlsval  22032  selvval  22061  evls1fval  22238  evl1fval  22247  pf1mpf  22271  pf1ind  22274  ofco2  22366  qtophmeo  23734  ustssco  24132  utop2nei  24168  neipcfilu  24214  tngds  24577  tngdsOLD  24578  elovolmr  25418  ovoliunlem3  25446  uniioombllem2  25525  hoddi  31813  fcoinver  32407  fmptco1f1o  32431  fcobij  32517  symgfcoeu  32818  symgcom  32819  tocycf  32851  tocyc01  32852  cycpmconjvlem  32875  cycpmconjv  32876  cycpmconjslem1  32888  cycpmconjslem2  32889  cycpmconjs  32890  cyc3conja  32891  smatfval  33396  eulerpartlemgv  33993  eulerpartlemn  34001  eulerpart  34002  sseqval  34008  reprpmtf1o  34258  erdsze2lem2  34814  cvmliftlem10  34904  mrsubval  35119  ftc1anclem8  37173  cocnv  37198  ltrncoidN  39601  trlcoabs2N  40195  cdlemg47a  40207  cdlemg46  40208  cdlemg47  40209  ltrnco4  40212  tendovalco  40238  tendoplcbv  40248  tendopl  40249  tendoplass  40256  cdlemi2  40292  cdlemk2  40305  cdlemk4  40307  cdlemk8  40311  cdlemkuu  40368  cdlemk53  40430  cdlemk54  40431  cdlemk55a  40432  erngdvlem3  40463  erngdvlem3-rN  40471  tendocnv  40494  tendospcanN  40496  dvhvaddcbv  40562  dvhvaddval  40563  dvhvaddass  40570  dvhvscacbv  40571  dvhvscaval  40572  dvhopvsca  40575  dvhlveclem  40581  dvhopspN  40588  diblss  40643  cdlemn8  40677  dihopelvalcpre  40721  dihmeetlem1N  40763  dihglblem5apreN  40764  dih1dimatlem0  40801  dihjatcclem4  40894  aks6d1c6lem5  41649  mhmcoaddmpl  41784  rhmcomulmpl  41785  rhmmpl  41786  diophrw  42179  eldioph2  42182  relexpaddss  43148  trclfvcom  43153  frege131d  43194  fsovrfovd  43439  hoicvrrex  45944  ovnlecvr  45946  ovncvrrp  45952  ovn0lem  45953  ovnsubaddlem1  45958  ovnsubadd  45960  ovnhoilem1  45989  ovnhoi  45991  ovnlecvr2  45998  ovncvr2  45999  hspmbl  46017  ovnovollem1  46044  ovnovollem3  46046

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »