Theorem coeq2d 5846

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

Syntax hints:   → wi 4   = wceq 1567   ∘ ccom 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5111  df-opab 5175  df-co 5668

This theorem is referenced by:  coeq12d  5848  dfpo2  6295  f1ococnv1  6848  funcoeqres  6850  fcof1oinvd  7289  foeqcnvco  7296  f1ofvswap  7302  coof  7696  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  17504  isofval  17810  cofuass  17942  cofurid  17944  fucid  18027  setcinv  18143  catcisolem  18163  curf2ndf  18299  pwsco2mhm  18888  symggrplem  18939  smndex1igid  18961  smndex1igidOLD  18962  f1omvdco2  19514  psgnunilem1  19559  efginvrel2  19793  efginvrel1  19794  vrgpinv  19835  frgpuplem  19838  gsumval3  19973  gsumzf1o  19978  psrass1lem  22048  mpfrcl  22201  evlsval  22202  selvval  22236  mhmcoaddmpl  22239  rhmcomulmpl  22240  evls1fval  22444  evl1fval  22453  pf1mpf  22477  pf1ind  22480  rhmmpl  22505  rhmply1vr1  22509  rhmply1vsca  22510  ofco2  22573  qtophmeo  23939  ustssco  24337  utop2nei  24372  neipcfilu  24417  tngds  24770  elovolmr  25600  ovoliunlem3  25628  uniioombllem2  25707  hoddi  32279  fcoinver  32886  fmptco1f1o  32915  fcobij  33002  cocnvf1o  33011  symgfcoeu  33339  symgcom  33340  tocycf  33374  tocyc01  33375  cycpmconjvlem  33398  cycpmconjv  33399  cycpmconjslem1  33411  cycpmconjslem2  33412  cycpmconjs  33413  cyc3conja  33414  1arithidomlem2  33767  selvascl  33848  mplvrpmga  33876  mplvrpmrhm  33878  esplyfval  33894  esplyfval0  33895  esplyfval2  33896  vieta  33911  smatfval  34126  eulerpartlemgv  34704  eulerpartlemn  34712  eulerpart  34713  sseqval  34719  reprpmtf1o  34954  erdsze2lem2  35591  cvmliftlem10  35681  mrsubval  35896  ftc1anclem8  38234  cocnv  38259  ltrncoidN  40787  trlcoabs2N  41381  cdlemg47a  41393  cdlemg46  41394  cdlemg47  41395  ltrnco4  41398  tendovalco  41424  tendoplcbv  41434  tendopl  41435  tendoplass  41442  cdlemi2  41478  cdlemk2  41491  cdlemk4  41493  cdlemk8  41497  cdlemkuu  41554  cdlemk53  41616  cdlemk54  41617  cdlemk55a  41618  erngdvlem3  41649  erngdvlem3-rN  41657  tendocnv  41680  tendospcanN  41682  dvhvaddcbv  41748  dvhvaddval  41749  dvhvaddass  41756  dvhvscacbv  41757  dvhvscaval  41758  dvhopvsca  41761  dvhlveclem  41767  dvhopspN  41774  diblss  41829  cdlemn8  41863  dihopelvalcpre  41907  dihmeetlem1N  41949  dihglblem5apreN  41950  dih1dimatlem0  41987  dihjatcclem4  42080  aks6d1c6lem5  42829  mhmcoaddpsr  43200  rhmcomulpsr  43201  rhmpsr  43202  diophrw  43377  eldioph2  43380  relexpaddss  44331  trclfvcom  44336  frege131d  44377  fsovrfovd  44622  hoicvrrex  47157  ovnlecvr  47159  ovncvrrp  47165  ovn0lem  47166  ovnsubaddlem1  47171  ovnsubadd  47173  ovnhoilem1  47202  ovnhoi  47204  ovnlecvr2  47211  ovncvr2  47212  hspmbl  47230  ovnovollem1  47257  ovnovollem3  47259  3f1oss2  47697  cosn  49492  fuco11id  49992  fucoid  50006  precofval3  50029  prcofvalg  50034  prcofval  50036