Theorem coeq2d 5731

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

Syntax hints:   → wi 4   = wceq 1543   ∘ ccom 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-br 5054  df-opab 5116  df-co 5560

This theorem is referenced by:  coeq12d  5733  f1ococnv1  6689  funcoeqres  6691  fcof1oinvd  7103  foeqcnvco  7110  f1ofvswap  7116  fparlem3  7882  fparlem4  7883  offsplitfpar  7888  mapen  8810  mapfien  9024  wemapwe  9312  hashfacen  14018  hashfacenOLD  14019  s1co  14398  pfxco  14403  relexpsucnnl  14593  relexpsucl  14594  relexpsucld  14597  relexpcnv  14598  relexpaddnn  14614  relexpaddg  14616  prdsval  16960  isofval  17262  cofuass  17395  cofurid  17397  fucid  17480  setcinv  17596  catcisolem  17616  curf2ndf  17755  pwsco2mhm  18259  symggrplem  18311  smndex1igid  18331  f1omvdco2  18840  psgnunilem1  18885  efginvrel2  19117  efginvrel1  19118  vrgpinv  19159  frgpuplem  19162  gsumval3  19292  gsumzf1o  19297  psrass1lemOLD  20899  psrass1lem  20902  mpfrcl  21045  evlsval  21046  selvval  21078  evls1fval  21235  evl1fval  21244  pf1mpf  21268  pf1ind  21271  ofco2  21348  qtophmeo  22714  ustssco  23112  utop2nei  23148  neipcfilu  23193  tngds  23546  elovolmr  24373  ovoliunlem3  24401  uniioombllem2  24480  hoddi  30071  fcoinver  30665  fmptco1f1o  30687  fcobij  30777  symgfcoeu  31070  symgcom  31071  tocycf  31103  tocyc01  31104  cycpmconjvlem  31127  cycpmconjv  31128  cycpmconjslem1  31140  cycpmconjslem2  31141  cycpmconjs  31142  cyc3conja  31143  smatfval  31459  eulerpartlemgv  32052  eulerpartlemn  32060  eulerpart  32061  sseqval  32067  reprpmtf1o  32318  erdsze2lem2  32879  cvmliftlem10  32969  mrsubval  33184  dfpo2  33441  ftc1anclem8  35594  cocnv  35620  ltrncoidN  37879  trlcoabs2N  38473  cdlemg47a  38485  cdlemg46  38486  cdlemg47  38487  ltrnco4  38490  tendovalco  38516  tendoplcbv  38526  tendopl  38527  tendoplass  38534  cdlemi2  38570  cdlemk2  38583  cdlemk4  38585  cdlemk8  38589  cdlemkuu  38646  cdlemk53  38708  cdlemk54  38709  cdlemk55a  38710  erngdvlem3  38741  erngdvlem3-rN  38749  tendocnv  38772  tendospcanN  38774  dvhvaddcbv  38840  dvhvaddval  38841  dvhvaddass  38848  dvhvscacbv  38849  dvhvscaval  38850  dvhopvsca  38853  dvhlveclem  38859  dvhopspN  38866  diblss  38921  cdlemn8  38955  dihopelvalcpre  38999  dihmeetlem1N  39041  dihglblem5apreN  39042  dih1dimatlem0  39079  dihjatcclem4  39172  diophrw  40284  eldioph2  40287  relexpaddss  41003  trclfvcom  41008  frege131d  41049  fsovrfovd  41294  hoicvrrex  43769  ovnlecvr  43771  ovncvrrp  43777  ovn0lem  43778  ovnsubaddlem1  43783  ovnsubadd  43785  ovnhoilem1  43814  ovnhoi  43816  ovnlecvr2  43823  ovncvr2  43824  hspmbl  43842  ovnovollem1  43869  ovnovollem3  43871