Theorem coeq2d 5808

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 5804	. 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 3915  df-br 5096  df-opab 5158  df-co 5630

This theorem is referenced by:  coeq12d  5810  dfpo2  6251  f1ococnv1  6800  funcoeqres  6802  fcof1oinvd  7236  foeqcnvco  7243  f1ofvswap  7249  coof  7643  fparlem3  8053  fparlem4  8054  offsplitfpar  8058  csbwrecsg  8257  mapen  9065  mapfien  9303  wemapwe  9598  hashfacen  14368  s1co  14747  pfxco  14752  relexpsucnnl  14944  relexpsucl  14945  relexpsucld  14948  relexpcnv  14949  relexpaddnn  14965  relexpaddg  14967  prdsval  17366  isofval  17672  cofuass  17804  cofurid  17806  fucid  17889  setcinv  18005  catcisolem  18025  curf2ndf  18161  pwsco2mhm  18749  symggrplem  18800  smndex1igid  18820  f1omvdco2  19368  psgnunilem1  19413  efginvrel2  19647  efginvrel1  19648  vrgpinv  19689  frgpuplem  19692  gsumval3  19827  gsumzf1o  19832  psrass1lem  21879  mpfrcl  22031  evlsval  22032  selvval  22069  evls1fval  22254  evl1fval  22263  pf1mpf  22287  pf1ind  22290  mhmcoaddmpl  22316  rhmcomulmpl  22317  rhmmpl  22318  rhmply1vr1  22322  rhmply1vsca  22323  ofco2  22386  qtophmeo  23752  ustssco  24150  utop2nei  24185  neipcfilu  24230  tngds  24583  elovolmr  25424  ovoliunlem3  25452  uniioombllem2  25531  hoddi  31991  fcoinver  32605  fmptco1f1o  32637  fcobij  32727  cocnvf1o  32736  symgfcoeu  33092  symgcom  33093  tocycf  33127  tocyc01  33128  cycpmconjvlem  33151  cycpmconjv  33152  cycpmconjslem1  33164  cycpmconjslem2  33165  cycpmconjs  33166  cyc3conja  33167  1arithidomlem2  33545  mplvrpmga  33638  mplvrpmrhm  33640  esplyfval  33649  esplyfval0  33650  esplyfval2  33651  vieta  33664  smatfval  33880  eulerpartlemgv  34458  eulerpartlemn  34466  eulerpart  34467  sseqval  34473  reprpmtf1o  34711  erdsze2lem2  35320  cvmliftlem10  35410  mrsubval  35625  ftc1anclem8  37813  cocnv  37838  ltrncoidN  40300  trlcoabs2N  40894  cdlemg47a  40906  cdlemg46  40907  cdlemg47  40908  ltrnco4  40911  tendovalco  40937  tendoplcbv  40947  tendopl  40948  tendoplass  40955  cdlemi2  40991  cdlemk2  41004  cdlemk4  41006  cdlemk8  41010  cdlemkuu  41067  cdlemk53  41129  cdlemk54  41130  cdlemk55a  41131  erngdvlem3  41162  erngdvlem3-rN  41170  tendocnv  41193  tendospcanN  41195  dvhvaddcbv  41261  dvhvaddval  41262  dvhvaddass  41269  dvhvscacbv  41270  dvhvscaval  41271  dvhopvsca  41274  dvhlveclem  41280  dvhopspN  41287  diblss  41342  cdlemn8  41376  dihopelvalcpre  41420  dihmeetlem1N  41462  dihglblem5apreN  41463  dih1dimatlem0  41500  dihjatcclem4  41593  aks6d1c6lem5  42343  mhmcoaddpsr  42718  rhmcomulpsr  42719  rhmpsr  42720  diophrw  42916  eldioph2  42919  relexpaddss  43875  trclfvcom  43880  frege131d  43921  fsovrfovd  44166  hoicvrrex  46716  ovnlecvr  46718  ovncvrrp  46724  ovn0lem  46725  ovnsubaddlem1  46730  ovnsubadd  46732  ovnhoilem1  46761  ovnhoi  46763  ovnlecvr2  46770  ovncvr2  46771  hspmbl  46789  ovnovollem1  46816  ovnovollem3  46818  3f1oss2  47238  cosn  48995  fuco11id  49495  fucoid  49509  precofval3  49532  prcofvalg  49537  prcofval  49539