Theorem coeq2d 5826

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

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-br 5108  df-opab 5170  df-co 5647

This theorem is referenced by:  coeq12d  5828  dfpo2  6269  f1ococnv1  6829  funcoeqres  6831  fcof1oinvd  7268  foeqcnvco  7275  f1ofvswap  7281  coof  7677  fparlem3  8093  fparlem4  8094  offsplitfpar  8098  csbwrecsg  8297  mapen  9105  mapfien  9359  wemapwe  9650  hashfacen  14419  s1co  14799  pfxco  14804  relexpsucnnl  14996  relexpsucl  14997  relexpsucld  15000  relexpcnv  15001  relexpaddnn  15017  relexpaddg  15019  prdsval  17418  isofval  17719  cofuass  17851  cofurid  17853  fucid  17936  setcinv  18052  catcisolem  18072  curf2ndf  18208  pwsco2mhm  18760  symggrplem  18811  smndex1igid  18831  f1omvdco2  19378  psgnunilem1  19423  efginvrel2  19657  efginvrel1  19658  vrgpinv  19699  frgpuplem  19702  gsumval3  19837  gsumzf1o  19842  psrass1lem  21841  mpfrcl  21992  evlsval  21993  selvval  22022  evls1fval  22206  evl1fval  22215  pf1mpf  22239  pf1ind  22242  mhmcoaddmpl  22268  rhmcomulmpl  22269  rhmmpl  22270  rhmply1vr1  22274  rhmply1vsca  22275  ofco2  22338  qtophmeo  23704  ustssco  24102  utop2nei  24138  neipcfilu  24183  tngds  24536  elovolmr  25377  ovoliunlem3  25405  uniioombllem2  25484  hoddi  31919  fcoinver  32533  fmptco1f1o  32557  fcobij  32645  symgfcoeu  33039  symgcom  33040  tocycf  33074  tocyc01  33075  cycpmconjvlem  33098  cycpmconjv  33099  cycpmconjslem1  33111  cycpmconjslem2  33112  cycpmconjs  33113  cyc3conja  33114  1arithidomlem2  33507  smatfval  33785  eulerpartlemgv  34364  eulerpartlemn  34372  eulerpart  34373  sseqval  34379  reprpmtf1o  34617  erdsze2lem2  35191  cvmliftlem10  35281  mrsubval  35496  ftc1anclem8  37694  cocnv  37719  ltrncoidN  40122  trlcoabs2N  40716  cdlemg47a  40728  cdlemg46  40729  cdlemg47  40730  ltrnco4  40733  tendovalco  40759  tendoplcbv  40769  tendopl  40770  tendoplass  40777  cdlemi2  40813  cdlemk2  40826  cdlemk4  40828  cdlemk8  40832  cdlemkuu  40889  cdlemk53  40951  cdlemk54  40952  cdlemk55a  40953  erngdvlem3  40984  erngdvlem3-rN  40992  tendocnv  41015  tendospcanN  41017  dvhvaddcbv  41083  dvhvaddval  41084  dvhvaddass  41091  dvhvscacbv  41092  dvhvscaval  41093  dvhopvsca  41096  dvhlveclem  41102  dvhopspN  41109  diblss  41164  cdlemn8  41198  dihopelvalcpre  41242  dihmeetlem1N  41284  dihglblem5apreN  41285  dih1dimatlem0  41322  dihjatcclem4  41415  aks6d1c6lem5  42165  mhmcoaddpsr  42538  rhmcomulpsr  42539  rhmpsr  42540  diophrw  42747  eldioph2  42750  relexpaddss  43707  trclfvcom  43712  frege131d  43753  fsovrfovd  43998  hoicvrrex  46554  ovnlecvr  46556  ovncvrrp  46562  ovn0lem  46563  ovnsubaddlem1  46568  ovnsubadd  46570  ovnhoilem1  46599  ovnhoi  46601  ovnlecvr2  46608  ovncvr2  46609  hspmbl  46627  ovnovollem1  46654  ovnovollem3  46656  3f1oss2  47077  cosn  48822  fuco11id  49323  fucoid  49337  precofval3  49360  prcofvalg  49365  prcofval  49367