Theorem coeq2d 5760

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 5756	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ∘ ccom 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-co 5589

This theorem is referenced by:  coeq12d  5762  dfpo2  6188  f1ococnv1  6728  funcoeqres  6730  fcof1oinvd  7145  foeqcnvco  7152  f1ofvswap  7158  fparlem3  7925  fparlem4  7926  offsplitfpar  7931  csbwrecsg  8108  mapen  8877  mapfien  9097  wemapwe  9385  hashfacen  14094  hashfacenOLD  14095  s1co  14474  pfxco  14479  relexpsucnnl  14669  relexpsucl  14670  relexpsucld  14673  relexpcnv  14674  relexpaddnn  14690  relexpaddg  14692  prdsval  17083  isofval  17386  cofuass  17520  cofurid  17522  fucid  17605  setcinv  17721  catcisolem  17741  curf2ndf  17881  pwsco2mhm  18386  symggrplem  18438  smndex1igid  18458  f1omvdco2  18971  psgnunilem1  19016  efginvrel2  19248  efginvrel1  19249  vrgpinv  19290  frgpuplem  19293  gsumval3  19423  gsumzf1o  19428  psrass1lemOLD  21053  psrass1lem  21056  mpfrcl  21205  evlsval  21206  selvval  21238  evls1fval  21395  evl1fval  21404  pf1mpf  21428  pf1ind  21431  ofco2  21508  qtophmeo  22876  ustssco  23274  utop2nei  23310  neipcfilu  23356  tngds  23717  tngdsOLD  23718  elovolmr  24545  ovoliunlem3  24573  uniioombllem2  24652  hoddi  30253  fcoinver  30847  fmptco1f1o  30869  fcobij  30959  symgfcoeu  31253  symgcom  31254  tocycf  31286  tocyc01  31287  cycpmconjvlem  31310  cycpmconjv  31311  cycpmconjslem1  31323  cycpmconjslem2  31324  cycpmconjs  31325  cyc3conja  31326  smatfval  31647  eulerpartlemgv  32240  eulerpartlemn  32248  eulerpart  32249  sseqval  32255  reprpmtf1o  32506  erdsze2lem2  33066  cvmliftlem10  33156  mrsubval  33371  ftc1anclem8  35784  cocnv  35810  ltrncoidN  38069  trlcoabs2N  38663  cdlemg47a  38675  cdlemg46  38676  cdlemg47  38677  ltrnco4  38680  tendovalco  38706  tendoplcbv  38716  tendopl  38717  tendoplass  38724  cdlemi2  38760  cdlemk2  38773  cdlemk4  38775  cdlemk8  38779  cdlemkuu  38836  cdlemk53  38898  cdlemk54  38899  cdlemk55a  38900  erngdvlem3  38931  erngdvlem3-rN  38939  tendocnv  38962  tendospcanN  38964  dvhvaddcbv  39030  dvhvaddval  39031  dvhvaddass  39038  dvhvscacbv  39039  dvhvscaval  39040  dvhopvsca  39043  dvhlveclem  39049  dvhopspN  39056  diblss  39111  cdlemn8  39145  dihopelvalcpre  39189  dihmeetlem1N  39231  dihglblem5apreN  39232  dih1dimatlem0  39269  dihjatcclem4  39362  diophrw  40497  eldioph2  40500  relexpaddss  41215  trclfvcom  41220  frege131d  41261  fsovrfovd  41506  hoicvrrex  43984  ovnlecvr  43986  ovncvrrp  43992  ovn0lem  43993  ovnsubaddlem1  43998  ovnsubadd  44000  ovnhoilem1  44029  ovnhoi  44031  ovnlecvr2  44038  ovncvr2  44039  hspmbl  44057  ovnovollem1  44084  ovnovollem3  44086