Theorem coeq2d 5797

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

Syntax hints:   → wi 4   = wceq 1541   ∘ ccom 5615

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5087  df-opab 5149  df-co 5620

This theorem is referenced by:  coeq12d  5799  dfpo2  6238  f1ococnv1  6787  funcoeqres  6789  fcof1oinvd  7222  foeqcnvco  7229  f1ofvswap  7235  coof  7629  fparlem3  8039  fparlem4  8040  offsplitfpar  8044  csbwrecsg  8243  mapen  9049  mapfien  9287  wemapwe  9582  hashfacen  14356  s1co  14735  pfxco  14740  relexpsucnnl  14932  relexpsucl  14933  relexpsucld  14936  relexpcnv  14937  relexpaddnn  14953  relexpaddg  14955  prdsval  17354  isofval  17659  cofuass  17791  cofurid  17793  fucid  17876  setcinv  17992  catcisolem  18012  curf2ndf  18148  pwsco2mhm  18736  symggrplem  18787  smndex1igid  18807  f1omvdco2  19355  psgnunilem1  19400  efginvrel2  19634  efginvrel1  19635  vrgpinv  19676  frgpuplem  19679  gsumval3  19814  gsumzf1o  19819  psrass1lem  21864  mpfrcl  22015  evlsval  22016  selvval  22045  evls1fval  22229  evl1fval  22238  pf1mpf  22262  pf1ind  22265  mhmcoaddmpl  22291  rhmcomulmpl  22292  rhmmpl  22293  rhmply1vr1  22297  rhmply1vsca  22298  ofco2  22361  qtophmeo  23727  ustssco  24125  utop2nei  24160  neipcfilu  24205  tngds  24558  elovolmr  25399  ovoliunlem3  25427  uniioombllem2  25506  hoddi  31962  fcoinver  32576  fmptco1f1o  32607  fcobij  32695  cocnvf1o  32704  symgfcoeu  33043  symgcom  33044  tocycf  33078  tocyc01  33079  cycpmconjvlem  33102  cycpmconjv  33103  cycpmconjslem1  33115  cycpmconjslem2  33116  cycpmconjs  33117  cyc3conja  33118  1arithidomlem2  33493  mplvrpmga  33567  mplvrpmrhm  33569  esplyfval  33578  smatfval  33800  eulerpartlemgv  34378  eulerpartlemn  34386  eulerpart  34387  sseqval  34393  reprpmtf1o  34631  erdsze2lem2  35240  cvmliftlem10  35330  mrsubval  35545  ftc1anclem8  37740  cocnv  37765  ltrncoidN  40167  trlcoabs2N  40761  cdlemg47a  40773  cdlemg46  40774  cdlemg47  40775  ltrnco4  40778  tendovalco  40804  tendoplcbv  40814  tendopl  40815  tendoplass  40822  cdlemi2  40858  cdlemk2  40871  cdlemk4  40873  cdlemk8  40877  cdlemkuu  40934  cdlemk53  40996  cdlemk54  40997  cdlemk55a  40998  erngdvlem3  41029  erngdvlem3-rN  41037  tendocnv  41060  tendospcanN  41062  dvhvaddcbv  41128  dvhvaddval  41129  dvhvaddass  41136  dvhvscacbv  41137  dvhvscaval  41138  dvhopvsca  41141  dvhlveclem  41147  dvhopspN  41154  diblss  41209  cdlemn8  41243  dihopelvalcpre  41287  dihmeetlem1N  41329  dihglblem5apreN  41330  dih1dimatlem0  41367  dihjatcclem4  41460  aks6d1c6lem5  42210  mhmcoaddpsr  42583  rhmcomulpsr  42584  rhmpsr  42585  diophrw  42792  eldioph2  42795  relexpaddss  43751  trclfvcom  43756  frege131d  43797  fsovrfovd  44042  hoicvrrex  46594  ovnlecvr  46596  ovncvrrp  46602  ovn0lem  46603  ovnsubaddlem1  46608  ovnsubadd  46610  ovnhoilem1  46639  ovnhoi  46641  ovnlecvr2  46648  ovncvr2  46649  hspmbl  46667  ovnovollem1  46694  ovnovollem3  46696  3f1oss2  47107  cosn  48865  fuco11id  49366  fucoid  49380  precofval3  49403  prcofvalg  49408  prcofval  49410