Theorem coeq2d 5850

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∘ ccom 5667

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-co 5672

This theorem is used by:  coeq12d  5852  dfpo2  6301  f1ococnv1  6854  funcoeqres  6856  fcof1oinvd  7300  foeqcnvco  7307  f1ofvswap  7313  coof  7708  fparlem3  8115  fparlem4  8116  offsplitfpar  8120  csbwrecsg  8321  mapen  9136  mapfien  9375  wemapwe  9673  hashfacen  14509  s1co  14894  pfxco  14899  relexpsucnnl  15091  relexpsucl  15092  relexpsucld  15095  relexpcnv  15096  relexpaddnn  15112  relexpaddg  15114  prdsval  17530  isofval  17836  cofuass  17968  cofurid  17970  fucid  18053  setcinv  18169  catcisolem  18189  curf2ndf  18325  pwsco2mhm  18929  symggrplem  18980  smndex1igid  19002  smndex1igidOLD  19003  f1omvdco2  19562  psgnunilem1  19607  efginvrel2  19841  efginvrel1  19842  vrgpinv  19883  frgpuplem  19886  gsumval3  20021  gsumzf1o  20026  psrass1lem  22133  mpfrcl  22286  evlsval  22287  selvval  22321  mhmcoaddmpl  22324  rhmcomulmpl  22325  evls1fval  22529  evl1fval  22538  pf1mpf  22562  pf1ind  22565  rhmmpl  22590  rhmply1vr1  22594  rhmply1vsca  22595  ofco2  22658  qtophmeo  24025  ustssco  24423  utop2nei  24458  neipcfilu  24503  tngds  24856  elovolmr  25686  ovoliunlem3  25714  uniioombllem2  25793  hoddi  32413  fcoinver  33020  fmptco1f1o  33049  fcobij  33135  cocnvf1o  33144  symgfcoeu  33466  symgcom  33467  tocycf  33501  tocyc01  33502  cycpmconjvlem  33525  cycpmconjv  33526  cycpmconjslem1  33538  cycpmconjslem2  33539  cycpmconjs  33540  cyc3conja  33541  1arithidomlem2  33890  selvascl  33971  mplvrpmga  33999  mplvrpmrhm  34001  esplyfval  34017  esplyfval0  34018  esplyfval2  34019  vieta  34034  smatfval  34249  eulerpartlemgv  34828  eulerpartlemn  34836  eulerpart  34837  sseqval  34843  reprpmtf1o  35078  erdsze2lem2  35733  cvmliftlem10  35823  mrsubval  36038  ftc1anclem8  38408  cocnv  38434  ltrncoidN  40960  trlcoabs2N  41554  cdlemg47a  41566  cdlemg46  41567  cdlemg47  41568  ltrnco4  41571  tendovalco  41597  tendoplcbv  41607  tendopl  41608  tendoplass  41615  cdlemi2  41651  cdlemk2  41664  cdlemk4  41666  cdlemk8  41670  cdlemkuu  41727  cdlemk53  41789  cdlemk54  41790  cdlemk55a  41791  erngdvlem3  41822  erngdvlem3-rN  41830  tendocnv  41853  tendospcanN  41855  dvhvaddcbv  41921  dvhvaddval  41922  dvhvaddass  41929  dvhvscacbv  41930  dvhvscaval  41931  dvhopvsca  41934  dvhlveclem  41940  dvhopspN  41947  diblss  42002  cdlemn8  42036  dihopelvalcpre  42080  dihmeetlem1N  42122  dihglblem5apreN  42123  dih1dimatlem0  42160  dihjatcclem4  42253  aks6d1c6lem5  43002  mhmcoaddpsr  43371  rhmcomulpsr  43372  rhmpsr  43373  diophrw  43548  eldioph2  43551  relexpaddss  44502  trclfvcom  44507  frege131d  44548  fsovrfovd  44793  hoicvrrex  47328  ovnlecvr  47330  ovncvrrp  47336  ovn0lem  47337  ovnsubaddlem1  47342  ovnsubadd  47344  ovnhoilem1  47373  ovnhoi  47375  ovnlecvr2  47382  ovncvr2  47383  hspmbl  47401  ovnovollem1  47428  ovnovollem3  47430  3f1oss2  47871  cosn  49669  fuco11id  50169  fucoid  50183  precofval3  50206  prcofvalg  50211  prcofval  50213