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 1541   ∘ ccom 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3916  df-br 5096  df-opab 5158  df-co 5630

This theorem is referenced by:  coeq12d  5811  dfpo2  6251  f1ococnv1  6800  funcoeqres  6802  fcof1oinvd  7236  foeqcnvco  7243  f1ofvswap  7249  coof  7643  fparlem3  8053  fparlem4  8054  offsplitfpar  8058  csbwrecsg  8257  mapen  9064  mapfien  9302  wemapwe  9597  hashfacen  14371  s1co  14750  pfxco  14755  relexpsucnnl  14947  relexpsucl  14948  relexpsucld  14951  relexpcnv  14952  relexpaddnn  14968  relexpaddg  14970  prdsval  17369  isofval  17674  cofuass  17806  cofurid  17808  fucid  17891  setcinv  18007  catcisolem  18027  curf2ndf  18163  pwsco2mhm  18751  symggrplem  18802  smndex1igid  18822  f1omvdco2  19370  psgnunilem1  19415  efginvrel2  19649  efginvrel1  19650  vrgpinv  19691  frgpuplem  19694  gsumval3  19829  gsumzf1o  19834  psrass1lem  21879  mpfrcl  22030  evlsval  22031  selvval  22060  evls1fval  22244  evl1fval  22253  pf1mpf  22277  pf1ind  22280  mhmcoaddmpl  22306  rhmcomulmpl  22307  rhmmpl  22308  rhmply1vr1  22312  rhmply1vsca  22313  ofco2  22376  qtophmeo  23742  ustssco  24140  utop2nei  24175  neipcfilu  24220  tngds  24573  elovolmr  25414  ovoliunlem3  25442  uniioombllem2  25521  hoddi  31981  fcoinver  32595  fmptco1f1o  32626  fcobij  32714  cocnvf1o  32723  symgfcoeu  33062  symgcom  33063  tocycf  33097  tocyc01  33098  cycpmconjvlem  33121  cycpmconjv  33122  cycpmconjslem1  33134  cycpmconjslem2  33135  cycpmconjs  33136  cyc3conja  33137  1arithidomlem2  33512  mplvrpmga  33586  mplvrpmrhm  33588  esplyfval  33597  smatfval  33819  eulerpartlemgv  34397  eulerpartlemn  34405  eulerpart  34406  sseqval  34412  reprpmtf1o  34650  erdsze2lem2  35259  cvmliftlem10  35349  mrsubval  35564  ftc1anclem8  37750  cocnv  37775  ltrncoidN  40237  trlcoabs2N  40831  cdlemg47a  40843  cdlemg46  40844  cdlemg47  40845  ltrnco4  40848  tendovalco  40874  tendoplcbv  40884  tendopl  40885  tendoplass  40892  cdlemi2  40928  cdlemk2  40941  cdlemk4  40943  cdlemk8  40947  cdlemkuu  41004  cdlemk53  41066  cdlemk54  41067  cdlemk55a  41068  erngdvlem3  41099  erngdvlem3-rN  41107  tendocnv  41130  tendospcanN  41132  dvhvaddcbv  41198  dvhvaddval  41199  dvhvaddass  41206  dvhvscacbv  41207  dvhvscaval  41208  dvhopvsca  41211  dvhlveclem  41217  dvhopspN  41224  diblss  41279  cdlemn8  41313  dihopelvalcpre  41357  dihmeetlem1N  41399  dihglblem5apreN  41400  dih1dimatlem0  41437  dihjatcclem4  41530  aks6d1c6lem5  42280  mhmcoaddpsr  42658  rhmcomulpsr  42659  rhmpsr  42660  diophrw  42866  eldioph2  42869  relexpaddss  43825  trclfvcom  43830  frege131d  43871  fsovrfovd  44116  hoicvrrex  46668  ovnlecvr  46670  ovncvrrp  46676  ovn0lem  46677  ovnsubaddlem1  46682  ovnsubadd  46684  ovnhoilem1  46713  ovnhoi  46715  ovnlecvr2  46722  ovncvr2  46723  hspmbl  46741  ovnovollem1  46768  ovnovollem3  46770  3f1oss2  47190  cosn  48948  fuco11id  49449  fucoid  49463  precofval3  49486  prcofvalg  49491  prcofval  49493