Theorem coeq2d 5848

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

Syntax hints:   → wi 4   = wceq 1570   ∘ ccom 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-co 5670

This theorem is referenced by:  coeq12d  5850  dfpo2  6297  f1ococnv1  6850  funcoeqres  6852  fcof1oinvd  7291  foeqcnvco  7298  f1ofvswap  7304  coof  7698  fparlem3  8105  fparlem4  8106  offsplitfpar  8110  csbwrecsg  8311  mapen  9125  mapfien  9364  wemapwe  9662  hashfacen  14487  s1co  14866  pfxco  14871  relexpsucnnl  15063  relexpsucl  15064  relexpsucld  15067  relexpcnv  15068  relexpaddnn  15084  relexpaddg  15086  prdsval  17503  isofval  17809  cofuass  17941  cofurid  17943  fucid  18026  setcinv  18142  catcisolem  18162  curf2ndf  18298  pwsco2mhm  18887  symggrplem  18938  smndex1igid  18960  smndex1igidOLD  18961  f1omvdco2  19513  psgnunilem1  19558  efginvrel2  19792  efginvrel1  19793  vrgpinv  19834  frgpuplem  19837  gsumval3  19972  gsumzf1o  19977  psrass1lem  22083  mpfrcl  22236  evlsval  22237  selvval  22271  mhmcoaddmpl  22274  rhmcomulmpl  22275  evls1fval  22479  evl1fval  22488  pf1mpf  22512  pf1ind  22515  rhmmpl  22540  rhmply1vr1  22544  rhmply1vsca  22545  ofco2  22608  qtophmeo  23974  ustssco  24372  utop2nei  24407  neipcfilu  24452  tngds  24805  elovolmr  25635  ovoliunlem3  25663  uniioombllem2  25742  hoddi  32342  fcoinver  32949  fmptco1f1o  32978  fcobij  33065  cocnvf1o  33074  symgfcoeu  33402  symgcom  33403  tocycf  33437  tocyc01  33438  cycpmconjvlem  33461  cycpmconjv  33462  cycpmconjslem1  33474  cycpmconjslem2  33475  cycpmconjs  33476  cyc3conja  33477  1arithidomlem2  33826  selvascl  33907  mplvrpmga  33935  mplvrpmrhm  33937  esplyfval  33953  esplyfval0  33954  esplyfval2  33955  vieta  33970  smatfval  34185  eulerpartlemgv  34763  eulerpartlemn  34771  eulerpart  34772  sseqval  34778  reprpmtf1o  35013  erdsze2lem2  35696  cvmliftlem10  35786  mrsubval  36001  ftc1anclem8  38351  cocnv  38376  ltrncoidN  40902  trlcoabs2N  41496  cdlemg47a  41508  cdlemg46  41509  cdlemg47  41510  ltrnco4  41513  tendovalco  41539  tendoplcbv  41549  tendopl  41550  tendoplass  41557  cdlemi2  41593  cdlemk2  41606  cdlemk4  41608  cdlemk8  41612  cdlemkuu  41669  cdlemk53  41731  cdlemk54  41732  cdlemk55a  41733  erngdvlem3  41764  erngdvlem3-rN  41772  tendocnv  41795  tendospcanN  41797  dvhvaddcbv  41863  dvhvaddval  41864  dvhvaddass  41871  dvhvscacbv  41872  dvhvscaval  41873  dvhopvsca  41876  dvhlveclem  41882  dvhopspN  41889  diblss  41944  cdlemn8  41978  dihopelvalcpre  42022  dihmeetlem1N  42064  dihglblem5apreN  42065  dih1dimatlem0  42102  dihjatcclem4  42195  aks6d1c6lem5  42944  mhmcoaddpsr  43313  rhmcomulpsr  43314  rhmpsr  43315  diophrw  43490  eldioph2  43493  relexpaddss  44444  trclfvcom  44449  frege131d  44490  fsovrfovd  44735  hoicvrrex  47270  ovnlecvr  47272  ovncvrrp  47278  ovn0lem  47279  ovnsubaddlem1  47284  ovnsubadd  47286  ovnhoilem1  47315  ovnhoi  47317  ovnlecvr2  47324  ovncvr2  47325  hspmbl  47343  ovnovollem1  47370  ovnovollem3  47372  3f1oss2  47813  cosn  49612  fuco11id  50112  fucoid  50126  precofval3  50149  prcofvalg  50154  prcofval  50156