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 1569   ∘ ccom 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3897  df-br 5103  df-opab 5167  df-co 5659

This theorem is used by:  coeq12d  5842  dfpo2  6301  f1ococnv1  6857  funcoeqres  6859  fcof1oinvd  7303  foeqcnvco  7310  f1ofvswap  7316  coof  7719  fparlem3  8129  fparlem4  8130  offsplitfpar  8134  csbwrecsg  8341  mapen  9165  mapfien  9405  wemapwe  9703  hashfacen  14604  s1co  14990  pfxco  14995  relexpsucnnl  15190  relexpsucl  15191  relexpsucld  15194  relexpcnv  15195  relexpaddnn  15211  relexpaddg  15213  prdsval  17633  isofval  17939  cofuass  18071  cofurid  18073  fucid  18156  setcinv  18272  catcisolem  18292  curf2ndf  18428  pwsco2mhm  19036  symggrplem  19087  smndex1igid  19109  smndex1igidOLD  19110  f1omvdco2  19669  psgnunilem1  19714  efginvrel2  19948  efginvrel1  19949  vrgpinv  19990  frgpuplem  19993  gsumval3  20128  gsumzf1o  20133  psrass1lem  22248  mpfrcl  22401  evlsval  22402  selvval  22436  mhmcoaddmpl  22439  rhmcomulmpl  22440  evls1fval  22644  evl1fval  22653  pf1mpf  22677  pf1ind  22680  rhmmpl  22705  rhmply1vr1  22709  rhmply1vsca  22710  ofco2  22773  qtophmeo  24143  ustssco  24541  utop2nei  24576  neipcfilu  24621  tngds  24974  elovolmr  25804  ovoliunlem3  25832  uniioombllem2  25911  hoddi  32599  fcoinver  33247  fmptco1f1o  33276  fcobij  33360  cocnvf1o  33369  symgfcoeu  33691  symgcom  33692  tocycf  33726  tocyc01  33727  cycpmconjvlem  33750  cycpmconjv  33751  cycpmconjslem1  33763  cycpmconjslem2  33764  cycpmconjs  33765  cyc3conja  33766  1arithidomlem2  34116  selvascl  34197  mplvrpmga  34225  mplvrpmrhm  34227  esplyfval  34243  esplyfval0  34244  esplyfval2  34245  vieta  34260  smatfval  34475  eulerpartlemgv  35053  eulerpartlemn  35061  eulerpart  35062  sseqval  35068  reprpmtf1o  35303  erdsze2lem2  36057  cvmliftlem10  36147  mrsubval  36362  ftc1anclem8  38725  cocnv  38766  ltrncoidN  41292  trlcoabs2N  41886  cdlemg47a  41898  cdlemg46  41899  cdlemg47  41900  ltrnco4  41903  tendovalco  41929  tendoplcbv  41939  tendopl  41940  tendoplass  41947  cdlemi2  41983  cdlemk2  41996  cdlemk4  41998  cdlemk8  42002  cdlemkuu  42059  cdlemk53  42121  cdlemk54  42122  cdlemk55a  42123  erngdvlem3  42154  erngdvlem3-rN  42162  tendocnv  42185  tendospcanN  42187  dvhvaddcbv  42253  dvhvaddval  42254  dvhvaddass  42261  dvhvscacbv  42262  dvhvscaval  42263  dvhopvsca  42266  dvhlveclem  42272  dvhopspN  42279  diblss  42334  cdlemn8  42368  dihopelvalcpre  42412  dihmeetlem1N  42454  dihglblem5apreN  42455  dih1dimatlem0  42492  dihjatcclem4  42585  aks6d1c6lem5  43334  mhmcoaddpsr  43716  rhmcomulpsr  43717  rhmpsr  43718  diophrw  43877  eldioph2  43880  relexpaddss  44825  trclfvcom  44830  frege131d  44871  fsovrfovd  45116  hoicvrrex  47673  ovnlecvr  47675  ovncvrrp  47681  ovn0lem  47682  ovnsubaddlem1  47687  ovnsubadd  47689  ovnhoilem1  47718  ovnhoi  47720  ovnlecvr2  47727  ovncvr2  47728  hspmbl  47746  ovnovollem1  47773  ovnovollem3  47775  3f1oss2  48253  cosn  50052  fuco11id  50563  fucoid  50577  fucoridid  50593  precofval3  50613  prcofvalg  50618  prcofval  50620