Theorem coeq2d 5887

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

Syntax hints:   → wi 4   = wceq 1537   ∘ ccom 5704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  coeq12d  5889  dfpo2  6327  f1ococnv1  6891  funcoeqres  6893  fcof1oinvd  7329  foeqcnvco  7336  f1ofvswap  7342  coof  7737  fparlem3  8155  fparlem4  8156  offsplitfpar  8160  csbwrecsg  8362  mapen  9207  mapfien  9477  wemapwe  9766  hashfacen  14503  s1co  14882  pfxco  14887  relexpsucnnl  15079  relexpsucl  15080  relexpsucld  15083  relexpcnv  15084  relexpaddnn  15100  relexpaddg  15102  prdsval  17515  isofval  17818  cofuass  17953  cofurid  17955  fucid  18041  setcinv  18157  catcisolem  18177  curf2ndf  18317  pwsco2mhm  18868  symggrplem  18919  smndex1igid  18939  f1omvdco2  19490  psgnunilem1  19535  efginvrel2  19769  efginvrel1  19770  vrgpinv  19811  frgpuplem  19814  gsumval3  19949  gsumzf1o  19954  psrass1lem  21975  mpfrcl  22132  evlsval  22133  selvval  22162  evls1fval  22344  evl1fval  22353  pf1mpf  22377  pf1ind  22380  mhmcoaddmpl  22406  rhmcomulmpl  22407  rhmmpl  22408  rhmply1vr1  22412  rhmply1vsca  22413  ofco2  22478  qtophmeo  23846  ustssco  24244  utop2nei  24280  neipcfilu  24326  tngds  24689  tngdsOLD  24690  elovolmr  25530  ovoliunlem3  25558  uniioombllem2  25637  hoddi  32022  fcoinver  32626  fmptco1f1o  32652  fcobij  32736  symgfcoeu  33075  symgcom  33076  tocycf  33110  tocyc01  33111  cycpmconjvlem  33134  cycpmconjv  33135  cycpmconjslem1  33147  cycpmconjslem2  33148  cycpmconjs  33149  cyc3conja  33150  1arithidomlem2  33529  smatfval  33741  eulerpartlemgv  34338  eulerpartlemn  34346  eulerpart  34347  sseqval  34353  reprpmtf1o  34603  erdsze2lem2  35172  cvmliftlem10  35262  mrsubval  35477  ftc1anclem8  37660  cocnv  37685  ltrncoidN  40085  trlcoabs2N  40679  cdlemg47a  40691  cdlemg46  40692  cdlemg47  40693  ltrnco4  40696  tendovalco  40722  tendoplcbv  40732  tendopl  40733  tendoplass  40740  cdlemi2  40776  cdlemk2  40789  cdlemk4  40791  cdlemk8  40795  cdlemkuu  40852  cdlemk53  40914  cdlemk54  40915  cdlemk55a  40916  erngdvlem3  40947  erngdvlem3-rN  40955  tendocnv  40978  tendospcanN  40980  dvhvaddcbv  41046  dvhvaddval  41047  dvhvaddass  41054  dvhvscacbv  41055  dvhvscaval  41056  dvhopvsca  41059  dvhlveclem  41065  dvhopspN  41072  diblss  41127  cdlemn8  41161  dihopelvalcpre  41205  dihmeetlem1N  41247  dihglblem5apreN  41248  dih1dimatlem0  41285  dihjatcclem4  41378  aks6d1c6lem5  42134  mhmcoaddpsr  42505  rhmcomulpsr  42506  rhmpsr  42507  diophrw  42715  eldioph2  42718  relexpaddss  43680  trclfvcom  43685  frege131d  43726  fsovrfovd  43971  hoicvrrex  46477  ovnlecvr  46479  ovncvrrp  46485  ovn0lem  46486  ovnsubaddlem1  46491  ovnsubadd  46493  ovnhoilem1  46522  ovnhoi  46524  ovnlecvr2  46531  ovncvr2  46532  hspmbl  46550  ovnovollem1  46577  ovnovollem3  46579  3f1oss2  46991