Theorem coeq2d 5830

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

Syntax hints:   → wi 4   = wceq 1559   ∘ ccom 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3919  df-br 5098  df-opab 5160  df-co 5652

This theorem is referenced by:  coeq12d  5832  dfpo2  6278  f1ococnv1  6831  funcoeqres  6833  fcof1oinvd  7272  foeqcnvco  7279  f1ofvswap  7285  coof  7679  fparlem3  8087  fparlem4  8088  offsplitfpar  8092  csbwrecsg  8293  mapen  9107  mapfien  9348  wemapwe  9646  hashfacen  14461  s1co  14840  pfxco  14845  relexpsucnnl  15037  relexpsucl  15038  relexpsucld  15041  relexpcnv  15042  relexpaddnn  15058  relexpaddg  15060  prdsval  17475  isofval  17781  cofuass  17913  cofurid  17915  fucid  17998  setcinv  18114  catcisolem  18134  curf2ndf  18270  pwsco2mhm  18858  symggrplem  18909  smndex1igid  18931  smndex1igidOLD  18932  f1omvdco2  19479  psgnunilem1  19524  efginvrel2  19758  efginvrel1  19759  vrgpinv  19800  frgpuplem  19803  gsumval3  19938  gsumzf1o  19943  psrass1lem  21973  mpfrcl  22126  evlsval  22127  selvval  22161  mhmcoaddmpl  22164  rhmcomulmpl  22165  evls1fval  22370  evl1fval  22379  pf1mpf  22403  pf1ind  22406  rhmmpl  22431  rhmply1vr1  22435  rhmply1vsca  22436  ofco2  22499  qtophmeo  23865  ustssco  24263  utop2nei  24298  neipcfilu  24343  tngds  24696  elovolmr  25526  ovoliunlem3  25554  uniioombllem2  25633  hoddi  32150  fcoinver  32764  fmptco1f1o  32796  fcobij  32883  cocnvf1o  32892  symgfcoeu  33223  symgcom  33224  tocycf  33258  tocyc01  33259  cycpmconjvlem  33282  cycpmconjv  33283  cycpmconjslem1  33295  cycpmconjslem2  33296  cycpmconjs  33297  cyc3conja  33298  1arithidomlem2  33693  selvascl  33775  mplvrpmga  33803  mplvrpmrhm  33805  esplyfval  33821  esplyfval0  33822  esplyfval2  33823  vieta  33838  smatfval  34053  eulerpartlemgv  34631  eulerpartlemn  34639  eulerpart  34640  sseqval  34646  reprpmtf1o  34881  erdsze2lem2  35515  cvmliftlem10  35605  mrsubval  35820  ftc1anclem8  38160  cocnv  38185  ltrncoidN  40713  trlcoabs2N  41307  cdlemg47a  41319  cdlemg46  41320  cdlemg47  41321  ltrnco4  41324  tendovalco  41350  tendoplcbv  41360  tendopl  41361  tendoplass  41368  cdlemi2  41404  cdlemk2  41417  cdlemk4  41419  cdlemk8  41423  cdlemkuu  41480  cdlemk53  41542  cdlemk54  41543  cdlemk55a  41544  erngdvlem3  41575  erngdvlem3-rN  41583  tendocnv  41606  tendospcanN  41608  dvhvaddcbv  41674  dvhvaddval  41675  dvhvaddass  41682  dvhvscacbv  41683  dvhvscaval  41684  dvhopvsca  41687  dvhlveclem  41693  dvhopspN  41700  diblss  41755  cdlemn8  41789  dihopelvalcpre  41833  dihmeetlem1N  41875  dihglblem5apreN  41876  dih1dimatlem0  41913  dihjatcclem4  42006  aks6d1c6lem5  42755  mhmcoaddpsr  43124  rhmcomulpsr  43125  rhmpsr  43126  diophrw  43301  eldioph2  43304  relexpaddss  44255  trclfvcom  44260  frege131d  44301  fsovrfovd  44546  hoicvrrex  47091  ovnlecvr  47093  ovncvrrp  47099  ovn0lem  47100  ovnsubaddlem1  47105  ovnsubadd  47107  ovnhoilem1  47136  ovnhoi  47138  ovnlecvr2  47145  ovncvr2  47146  hspmbl  47164  ovnovollem1  47191  ovnovollem3  47193  3f1oss2  47631  cosn  49416  fuco11id  49916  fucoid  49930  precofval3  49953  prcofvalg  49958  prcofval  49960