Theorem coeq2d 5842

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-co 5664

This theorem is used by:  coeq12d  5844  dfpo2  6294  f1ococnv1  6847  funcoeqres  6849  fcof1oinvd  7294  foeqcnvco  7301  f1ofvswap  7307  coof  7702  fparlem3  8111  fparlem4  8112  offsplitfpar  8116  csbwrecsg  8317  mapen  9139  mapfien  9378  wemapwe  9676  hashfacen  14519  s1co  14904  pfxco  14909  relexpsucnnl  15103  relexpsucl  15104  relexpsucld  15107  relexpcnv  15108  relexpaddnn  15124  relexpaddg  15126  prdsval  17540  isofval  17846  cofuass  17978  cofurid  17980  fucid  18063  setcinv  18179  catcisolem  18199  curf2ndf  18335  pwsco2mhm  18942  symggrplem  18993  smndex1igid  19015  smndex1igidOLD  19016  f1omvdco2  19575  psgnunilem1  19620  efginvrel2  19854  efginvrel1  19855  vrgpinv  19896  frgpuplem  19899  gsumval3  20034  gsumzf1o  20039  psrass1lem  22148  mpfrcl  22301  evlsval  22302  selvval  22336  mhmcoaddmpl  22339  rhmcomulmpl  22340  evls1fval  22544  evl1fval  22553  pf1mpf  22577  pf1ind  22580  rhmmpl  22605  rhmply1vr1  22609  rhmply1vsca  22610  ofco2  22673  qtophmeo  24043  ustssco  24441  utop2nei  24476  neipcfilu  24521  tngds  24874  elovolmr  25704  ovoliunlem3  25732  uniioombllem2  25811  hoddi  32471  fcoinver  33077  fmptco1f1o  33106  fcobij  33191  cocnvf1o  33200  symgfcoeu  33522  symgcom  33523  tocycf  33557  tocyc01  33558  cycpmconjvlem  33581  cycpmconjv  33582  cycpmconjslem1  33594  cycpmconjslem2  33595  cycpmconjs  33596  cyc3conja  33597  1arithidomlem2  33946  selvascl  34027  mplvrpmga  34055  mplvrpmrhm  34057  esplyfval  34073  esplyfval0  34074  esplyfval2  34075  vieta  34090  smatfval  34305  eulerpartlemgv  34884  eulerpartlemn  34892  eulerpart  34893  sseqval  34899  reprpmtf1o  35134  erdsze2lem2  35783  cvmliftlem10  35873  mrsubval  36088  ftc1anclem8  38449  cocnv  38475  ltrncoidN  41001  trlcoabs2N  41595  cdlemg47a  41607  cdlemg46  41608  cdlemg47  41609  ltrnco4  41612  tendovalco  41638  tendoplcbv  41648  tendopl  41649  tendoplass  41656  cdlemi2  41692  cdlemk2  41705  cdlemk4  41707  cdlemk8  41711  cdlemkuu  41768  cdlemk53  41830  cdlemk54  41831  cdlemk55a  41832  erngdvlem3  41863  erngdvlem3-rN  41871  tendocnv  41894  tendospcanN  41896  dvhvaddcbv  41962  dvhvaddval  41963  dvhvaddass  41970  dvhvscacbv  41971  dvhvscaval  41972  dvhopvsca  41975  dvhlveclem  41981  dvhopspN  41988  diblss  42043  cdlemn8  42077  dihopelvalcpre  42121  dihmeetlem1N  42163  dihglblem5apreN  42164  dih1dimatlem0  42201  dihjatcclem4  42294  aks6d1c6lem5  43043  mhmcoaddpsr  43427  rhmcomulpsr  43428  rhmpsr  43429  diophrw  43604  eldioph2  43607  relexpaddss  44558  trclfvcom  44563  frege131d  44604  fsovrfovd  44849  hoicvrrex  47384  ovnlecvr  47386  ovncvrrp  47392  ovn0lem  47393  ovnsubaddlem1  47398  ovnsubadd  47400  ovnhoilem1  47429  ovnhoi  47431  ovnlecvr2  47438  ovncvr2  47439  hspmbl  47457  ovnovollem1  47484  ovnovollem3  47486  3f1oss2  47964  cosn  49762  fuco11id  50260  fucoid  50274  precofval3  50297  prcofvalg  50302  prcofval  50304