Theorem coeq2d 5851

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5109  df-opab 5174  df-co 5667

This theorem is used by:  coeq12d  5853  dfpo2  6325  f1ococnv1  6885  funcoeqres  6887  fcof1oinvd  7332  foeqcnvco  7339  f1ofvswap  7345  coof  7749  fparlem3  8162  fparlem4  8163  offsplitfpar  8167  csbwrecsg  8374  mapen  9198  mapfien  9437  wemapwe  9735  hashfacen  14640  s1co  15026  pfxco  15031  relexpsucnnl  15226  relexpsucl  15227  relexpsucld  15230  relexpcnv  15231  relexpaddnn  15247  relexpaddg  15249  prdsval  17676  isofval  17982  cofuass  18114  cofurid  18116  fucid  18199  setcinv  18315  catcisolem  18335  curf2ndf  18471  pwsco2mhm  19079  symggrplem  19130  smndex1igid  19152  smndex1igidOLD  19153  f1omvdco2  19713  psgnunilem1  19758  efginvrel2  19992  efginvrel1  19993  vrgpinv  20034  frgpuplem  20037  gsumval3  20172  gsumzf1o  20177  psrass1lem  22296  mpfrcl  22449  evlsval  22450  selvval  22484  mhmcoaddmpl  22487  rhmcomulmpl  22488  evls1fval  22692  evl1fval  22701  pf1mpf  22725  pf1ind  22728  rhmmpl  22753  rhmply1vr1  22757  rhmply1vsca  22758  ofco2  22821  qtophmeo  24191  ustssco  24589  utop2nei  24624  neipcfilu  24669  tngds  25022  elovolmr  25852  ovoliunlem3  25880  uniioombllem2  25959  hoddi  32649  fcoinver  33296  fmptco1f1o  33325  fcobij  33408  cocnvf1o  33417  symgfcoeu  33742  symgcom  33743  tocycf  33777  tocyc01  33778  cycpmconjvlem  33801  cycpmconjv  33802  cycpmconjslem1  33814  cycpmconjslem2  33815  cycpmconjs  33816  cyc3conja  33817  1arithidomlem2  34172  selvascl  34260  mplvrpmga  34288  mplvrpmrhm  34290  esplyfval  34306  esplyfval0  34307  esplyfval2  34308  vieta  34323  smatfval  34538  eulerpartlemgv  35116  eulerpartlemn  35124  eulerpart  35125  sseqval  35131  reprpmtf1o  35366  erdsze2lem2  36177  cvmliftlem10  36267  mrsubval  36482  coss1b  38216  nvo3  38230  ftc1anclem8  38886  cocnv  38927  ltrncoidN  41451  trlcoabs2N  42045  cdlemg47a  42057  cdlemg46  42058  cdlemg47  42059  ltrnco4  42062  tendovalco  42088  tendoplcbv  42098  tendopl  42099  tendoplass  42106  cdlemi2  42142  cdlemk2  42155  cdlemk4  42157  cdlemk8  42161  cdlemkuu  42218  cdlemk53  42280  cdlemk54  42281  cdlemk55a  42282  erngdvlem3  42313  erngdvlem3-rN  42321  tendocnv  42344  tendospcanN  42346  dvhvaddcbv  42412  dvhvaddval  42413  dvhvaddass  42420  dvhvscacbv  42421  dvhvscaval  42422  dvhopvsca  42425  dvhlveclem  42431  dvhopspN  42438  diblss  42493  cdlemn8  42527  dihopelvalcpre  42571  dihmeetlem1N  42613  dihglblem5apreN  42614  dih1dimatlem0  42651  dihjatcclem4  42744  aks6d1c6lem5  43493  mhmcoaddpsr  43875  rhmcomulpsr  43876  rhmpsr  43877  diophrw  44036  eldioph2  44039  relexpaddss  44979  trclfvcom  44984  frege131d  45025  fsovrfovd  45270  hoicvrrex  47839  ovnlecvr  47841  ovncvrrp  47847  ovn0lem  47848  ovnsubaddlem1  47853  ovnsubadd  47855  ovnhoilem1  47884  ovnhoi  47886  ovnlecvr2  47893  ovncvr2  47894  hspmbl  47912  ovnovollem1  47939  ovnovollem3  47941  3f1oss2  48419  cosn  50276  fuco11id  50787  fucoid  50801  fucoridid  50817  precofval3  50837  prcofvalg  50842  prcofval  50844