Theorem coeq2d 5840

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∘ ccom 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-co 5660

This theorem is used by:  coeq12d  5842  dfpo2  6298  f1ococnv1  6852  funcoeqres  6854  fcof1oinvd  7299  foeqcnvco  7306  f1ofvswap  7312  coof  7715  fparlem3  8123  fparlem4  8124  offsplitfpar  8128  csbwrecsg  8329  mapen  9153  mapfien  9393  wemapwe  9691  hashfacen  14592  s1co  14977  pfxco  14982  relexpsucnnl  15176  relexpsucl  15177  relexpsucld  15180  relexpcnv  15181  relexpaddnn  15197  relexpaddg  15199  prdsval  17619  isofval  17925  cofuass  18057  cofurid  18059  fucid  18142  setcinv  18258  catcisolem  18278  curf2ndf  18414  pwsco2mhm  19022  symggrplem  19073  smndex1igid  19095  smndex1igidOLD  19096  f1omvdco2  19655  psgnunilem1  19700  efginvrel2  19934  efginvrel1  19935  vrgpinv  19976  frgpuplem  19979  gsumval3  20114  gsumzf1o  20119  psrass1lem  22234  mpfrcl  22387  evlsval  22388  selvval  22422  mhmcoaddmpl  22425  rhmcomulmpl  22426  evls1fval  22630  evl1fval  22639  pf1mpf  22663  pf1ind  22666  rhmmpl  22691  rhmply1vr1  22695  rhmply1vsca  22696  ofco2  22759  qtophmeo  24129  ustssco  24527  utop2nei  24562  neipcfilu  24607  tngds  24960  elovolmr  25790  ovoliunlem3  25818  uniioombllem2  25897  hoddi  32585  fcoinver  33191  fmptco1f1o  33220  fcobij  33305  cocnvf1o  33314  symgfcoeu  33636  symgcom  33637  tocycf  33671  tocyc01  33672  cycpmconjvlem  33695  cycpmconjv  33696  cycpmconjslem1  33708  cycpmconjslem2  33709  cycpmconjs  33710  cyc3conja  33711  1arithidomlem2  34061  selvascl  34142  mplvrpmga  34170  mplvrpmrhm  34172  esplyfval  34188  esplyfval0  34189  esplyfval2  34190  vieta  34205  smatfval  34420  eulerpartlemgv  34998  eulerpartlemn  35006  eulerpart  35007  sseqval  35013  reprpmtf1o  35248  erdsze2lem2  35948  cvmliftlem10  36038  mrsubval  36253  ftc1anclem8  38598  cocnv  38639  ltrncoidN  41165  trlcoabs2N  41759  cdlemg47a  41771  cdlemg46  41772  cdlemg47  41773  ltrnco4  41776  tendovalco  41802  tendoplcbv  41812  tendopl  41813  tendoplass  41820  cdlemi2  41856  cdlemk2  41869  cdlemk4  41871  cdlemk8  41875  cdlemkuu  41932  cdlemk53  41994  cdlemk54  41995  cdlemk55a  41996  erngdvlem3  42027  erngdvlem3-rN  42035  tendocnv  42058  tendospcanN  42060  dvhvaddcbv  42126  dvhvaddval  42127  dvhvaddass  42134  dvhvscacbv  42135  dvhvscaval  42136  dvhopvsca  42139  dvhlveclem  42145  dvhopspN  42152  diblss  42207  cdlemn8  42241  dihopelvalcpre  42285  dihmeetlem1N  42327  dihglblem5apreN  42328  dih1dimatlem0  42365  dihjatcclem4  42458  aks6d1c6lem5  43207  mhmcoaddpsr  43589  rhmcomulpsr  43590  rhmpsr  43591  diophrw  43749  eldioph2  43752  relexpaddss  44703  trclfvcom  44708  frege131d  44749  fsovrfovd  44994  hoicvrrex  47535  ovnlecvr  47537  ovncvrrp  47543  ovn0lem  47544  ovnsubaddlem1  47549  ovnsubadd  47551  ovnhoilem1  47580  ovnhoi  47582  ovnlecvr2  47589  ovncvr2  47590  hspmbl  47608  ovnovollem1  47635  ovnovollem3  47637  3f1oss2  48115  cosn  49913  fuco11id  50411  fucoid  50425  precofval3  50448  prcofvalg  50453  prcofval  50455