Theorem coeq2d 5809

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

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

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 3922  df-br 5096  df-opab 5158  df-co 5632

This theorem is referenced by:  coeq12d  5811  dfpo2  6248  f1ococnv1  6797  funcoeqres  6799  fcof1oinvd  7234  foeqcnvco  7241  f1ofvswap  7247  coof  7641  fparlem3  8054  fparlem4  8055  offsplitfpar  8059  csbwrecsg  8258  mapen  9065  mapfien  9317  wemapwe  9612  hashfacen  14380  s1co  14759  pfxco  14764  relexpsucnnl  14956  relexpsucl  14957  relexpsucld  14960  relexpcnv  14961  relexpaddnn  14977  relexpaddg  14979  prdsval  17378  isofval  17683  cofuass  17815  cofurid  17817  fucid  17900  setcinv  18016  catcisolem  18036  curf2ndf  18172  pwsco2mhm  18726  symggrplem  18777  smndex1igid  18797  f1omvdco2  19346  psgnunilem1  19391  efginvrel2  19625  efginvrel1  19626  vrgpinv  19667  frgpuplem  19670  gsumval3  19805  gsumzf1o  19810  psrass1lem  21858  mpfrcl  22009  evlsval  22010  selvval  22039  evls1fval  22223  evl1fval  22232  pf1mpf  22256  pf1ind  22259  mhmcoaddmpl  22285  rhmcomulmpl  22286  rhmmpl  22287  rhmply1vr1  22291  rhmply1vsca  22292  ofco2  22355  qtophmeo  23721  ustssco  24119  utop2nei  24155  neipcfilu  24200  tngds  24553  elovolmr  25394  ovoliunlem3  25422  uniioombllem2  25501  hoddi  31953  fcoinver  32567  fmptco1f1o  32595  fcobij  32683  symgfcoeu  33043  symgcom  33044  tocycf  33078  tocyc01  33079  cycpmconjvlem  33102  cycpmconjv  33103  cycpmconjslem1  33115  cycpmconjslem2  33116  cycpmconjs  33117  cyc3conja  33118  1arithidomlem2  33492  mplvrpmga  33565  smatfval  33781  eulerpartlemgv  34360  eulerpartlemn  34368  eulerpart  34369  sseqval  34375  reprpmtf1o  34613  erdsze2lem2  35196  cvmliftlem10  35286  mrsubval  35501  ftc1anclem8  37699  cocnv  37724  ltrncoidN  40127  trlcoabs2N  40721  cdlemg47a  40733  cdlemg46  40734  cdlemg47  40735  ltrnco4  40738  tendovalco  40764  tendoplcbv  40774  tendopl  40775  tendoplass  40782  cdlemi2  40818  cdlemk2  40831  cdlemk4  40833  cdlemk8  40837  cdlemkuu  40894  cdlemk53  40956  cdlemk54  40957  cdlemk55a  40958  erngdvlem3  40989  erngdvlem3-rN  40997  tendocnv  41020  tendospcanN  41022  dvhvaddcbv  41088  dvhvaddval  41089  dvhvaddass  41096  dvhvscacbv  41097  dvhvscaval  41098  dvhopvsca  41101  dvhlveclem  41107  dvhopspN  41114  diblss  41169  cdlemn8  41203  dihopelvalcpre  41247  dihmeetlem1N  41289  dihglblem5apreN  41290  dih1dimatlem0  41327  dihjatcclem4  41420  aks6d1c6lem5  42170  mhmcoaddpsr  42543  rhmcomulpsr  42544  rhmpsr  42545  diophrw  42752  eldioph2  42755  relexpaddss  43711  trclfvcom  43716  frege131d  43757  fsovrfovd  44002  hoicvrrex  46557  ovnlecvr  46559  ovncvrrp  46565  ovn0lem  46566  ovnsubaddlem1  46571  ovnsubadd  46573  ovnhoilem1  46602  ovnhoi  46604  ovnlecvr2  46611  ovncvr2  46612  hspmbl  46630  ovnovollem1  46657  ovnovollem3  46659  3f1oss2  47080  cosn  48838  fuco11id  49339  fucoid  49353  precofval3  49376  prcofvalg  49381  prcofval  49383