Theorem coeq2d 5811

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-br 5099  df-opab 5161  df-co 5633

This theorem is referenced by:  coeq12d  5813  dfpo2  6254  f1ococnv1  6803  funcoeqres  6805  fcof1oinvd  7239  foeqcnvco  7246  f1ofvswap  7252  coof  7646  fparlem3  8056  fparlem4  8057  offsplitfpar  8061  csbwrecsg  8260  mapen  9069  mapfien  9311  wemapwe  9606  hashfacen  14377  s1co  14756  pfxco  14761  relexpsucnnl  14953  relexpsucl  14954  relexpsucld  14957  relexpcnv  14958  relexpaddnn  14974  relexpaddg  14976  prdsval  17375  isofval  17681  cofuass  17813  cofurid  17815  fucid  17898  setcinv  18014  catcisolem  18034  curf2ndf  18170  pwsco2mhm  18758  symggrplem  18809  smndex1igid  18829  f1omvdco2  19377  psgnunilem1  19422  efginvrel2  19656  efginvrel1  19657  vrgpinv  19698  frgpuplem  19701  gsumval3  19836  gsumzf1o  19841  psrass1lem  21888  mpfrcl  22040  evlsval  22041  selvval  22078  evls1fval  22263  evl1fval  22272  pf1mpf  22296  pf1ind  22299  mhmcoaddmpl  22325  rhmcomulmpl  22326  rhmmpl  22327  rhmply1vr1  22331  rhmply1vsca  22332  ofco2  22395  qtophmeo  23761  ustssco  24159  utop2nei  24194  neipcfilu  24239  tngds  24592  elovolmr  25433  ovoliunlem3  25461  uniioombllem2  25540  hoddi  32065  fcoinver  32679  fmptco1f1o  32711  fcobij  32799  cocnvf1o  32808  symgfcoeu  33164  symgcom  33165  tocycf  33199  tocyc01  33200  cycpmconjvlem  33223  cycpmconjv  33224  cycpmconjslem1  33236  cycpmconjslem2  33237  cycpmconjs  33238  cyc3conja  33239  1arithidomlem2  33617  mplvrpmga  33710  mplvrpmrhm  33712  esplyfval  33721  esplyfval0  33722  esplyfval2  33723  vieta  33736  smatfval  33952  eulerpartlemgv  34530  eulerpartlemn  34538  eulerpart  34539  sseqval  34545  reprpmtf1o  34783  erdsze2lem2  35398  cvmliftlem10  35488  mrsubval  35703  ftc1anclem8  37901  cocnv  37926  ltrncoidN  40388  trlcoabs2N  40982  cdlemg47a  40994  cdlemg46  40995  cdlemg47  40996  ltrnco4  40999  tendovalco  41025  tendoplcbv  41035  tendopl  41036  tendoplass  41043  cdlemi2  41079  cdlemk2  41092  cdlemk4  41094  cdlemk8  41098  cdlemkuu  41155  cdlemk53  41217  cdlemk54  41218  cdlemk55a  41219  erngdvlem3  41250  erngdvlem3-rN  41258  tendocnv  41281  tendospcanN  41283  dvhvaddcbv  41349  dvhvaddval  41350  dvhvaddass  41357  dvhvscacbv  41358  dvhvscaval  41359  dvhopvsca  41362  dvhlveclem  41368  dvhopspN  41375  diblss  41430  cdlemn8  41464  dihopelvalcpre  41508  dihmeetlem1N  41550  dihglblem5apreN  41551  dih1dimatlem0  41588  dihjatcclem4  41681  aks6d1c6lem5  42431  mhmcoaddpsr  42803  rhmcomulpsr  42804  rhmpsr  42805  diophrw  43001  eldioph2  43004  relexpaddss  43959  trclfvcom  43964  frege131d  44005  fsovrfovd  44250  hoicvrrex  46800  ovnlecvr  46802  ovncvrrp  46808  ovn0lem  46809  ovnsubaddlem1  46814  ovnsubadd  46816  ovnhoilem1  46845  ovnhoi  46847  ovnlecvr2  46854  ovncvr2  46855  hspmbl  46873  ovnovollem1  46900  ovnovollem3  46902  3f1oss2  47322  cosn  49079  fuco11id  49579  fucoid  49593  precofval3  49616  prcofvalg  49621  prcofval  49623