Theorem coeq2d 5842

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-co 5663

This theorem is referenced by:  coeq12d  5844  dfpo2  6285  f1ococnv1  6846  funcoeqres  6848  fcof1oinvd  7285  foeqcnvco  7292  f1ofvswap  7298  coof  7693  fparlem3  8111  fparlem4  8112  offsplitfpar  8116  csbwrecsg  8318  mapen  9153  mapfien  9418  wemapwe  9709  hashfacen  14470  s1co  14850  pfxco  14855  relexpsucnnl  15047  relexpsucl  15048  relexpsucld  15051  relexpcnv  15052  relexpaddnn  15068  relexpaddg  15070  prdsval  17467  isofval  17768  cofuass  17900  cofurid  17902  fucid  17985  setcinv  18101  catcisolem  18121  curf2ndf  18257  pwsco2mhm  18809  symggrplem  18860  smndex1igid  18880  f1omvdco2  19427  psgnunilem1  19472  efginvrel2  19706  efginvrel1  19707  vrgpinv  19748  frgpuplem  19751  gsumval3  19886  gsumzf1o  19891  psrass1lem  21890  mpfrcl  22041  evlsval  22042  selvval  22071  evls1fval  22255  evl1fval  22264  pf1mpf  22288  pf1ind  22291  mhmcoaddmpl  22317  rhmcomulmpl  22318  rhmmpl  22319  rhmply1vr1  22323  rhmply1vsca  22324  ofco2  22387  qtophmeo  23753  ustssco  24151  utop2nei  24187  neipcfilu  24232  tngds  24585  elovolmr  25427  ovoliunlem3  25455  uniioombllem2  25534  hoddi  31917  fcoinver  32531  fmptco1f1o  32557  fcobij  32645  symgfcoeu  33039  symgcom  33040  tocycf  33074  tocyc01  33075  cycpmconjvlem  33098  cycpmconjv  33099  cycpmconjslem1  33111  cycpmconjslem2  33112  cycpmconjs  33113  cyc3conja  33114  1arithidomlem2  33497  smatfval  33772  eulerpartlemgv  34351  eulerpartlemn  34359  eulerpart  34360  sseqval  34366  reprpmtf1o  34604  erdsze2lem2  35172  cvmliftlem10  35262  mrsubval  35477  ftc1anclem8  37670  cocnv  37695  ltrncoidN  40093  trlcoabs2N  40687  cdlemg47a  40699  cdlemg46  40700  cdlemg47  40701  ltrnco4  40704  tendovalco  40730  tendoplcbv  40740  tendopl  40741  tendoplass  40748  cdlemi2  40784  cdlemk2  40797  cdlemk4  40799  cdlemk8  40803  cdlemkuu  40860  cdlemk53  40922  cdlemk54  40923  cdlemk55a  40924  erngdvlem3  40955  erngdvlem3-rN  40963  tendocnv  40986  tendospcanN  40988  dvhvaddcbv  41054  dvhvaddval  41055  dvhvaddass  41062  dvhvscacbv  41063  dvhvscaval  41064  dvhopvsca  41067  dvhlveclem  41073  dvhopspN  41080  diblss  41135  cdlemn8  41169  dihopelvalcpre  41213  dihmeetlem1N  41255  dihglblem5apreN  41256  dih1dimatlem0  41293  dihjatcclem4  41386  aks6d1c6lem5  42136  mhmcoaddpsr  42520  rhmcomulpsr  42521  rhmpsr  42522  diophrw  42729  eldioph2  42732  relexpaddss  43689  trclfvcom  43694  frege131d  43735  fsovrfovd  43980  hoicvrrex  46533  ovnlecvr  46535  ovncvrrp  46541  ovn0lem  46542  ovnsubaddlem1  46547  ovnsubadd  46549  ovnhoilem1  46578  ovnhoi  46580  ovnlecvr2  46587  ovncvr2  46588  hspmbl  46606  ovnovollem1  46633  ovnovollem3  46635  3f1oss2  47053  cosn  48760  fuco11id  49193  fucoid  49207  precofval3  49230  prcofvalg  49235  prcofval  49237