Theorem coeq2d 5774

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

Syntax hints:   → wi 4   = wceq 1539   ∘ ccom 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-br 5076  df-opab 5138  df-co 5599

This theorem is referenced by:  coeq12d  5776  dfpo2  6203  f1ococnv1  6754  funcoeqres  6756  fcof1oinvd  7174  foeqcnvco  7181  f1ofvswap  7187  fparlem3  7963  fparlem4  7964  offsplitfpar  7969  csbwrecsg  8146  mapen  8937  mapfien  9176  wemapwe  9464  hashfacen  14175  hashfacenOLD  14176  s1co  14555  pfxco  14560  relexpsucnnl  14750  relexpsucl  14751  relexpsucld  14754  relexpcnv  14755  relexpaddnn  14771  relexpaddg  14773  prdsval  17175  isofval  17478  cofuass  17613  cofurid  17615  fucid  17698  setcinv  17814  catcisolem  17834  curf2ndf  17974  pwsco2mhm  18480  symggrplem  18532  smndex1igid  18552  f1omvdco2  19065  psgnunilem1  19110  efginvrel2  19342  efginvrel1  19343  vrgpinv  19384  frgpuplem  19387  gsumval3  19517  gsumzf1o  19522  psrass1lemOLD  21152  psrass1lem  21155  mpfrcl  21304  evlsval  21305  selvval  21337  evls1fval  21494  evl1fval  21503  pf1mpf  21527  pf1ind  21530  ofco2  21609  qtophmeo  22977  ustssco  23375  utop2nei  23411  neipcfilu  23457  tngds  23820  tngdsOLD  23821  elovolmr  24649  ovoliunlem3  24677  uniioombllem2  24756  hoddi  30361  fcoinver  30955  fmptco1f1o  30977  fcobij  31066  symgfcoeu  31360  symgcom  31361  tocycf  31393  tocyc01  31394  cycpmconjvlem  31417  cycpmconjv  31418  cycpmconjslem1  31430  cycpmconjslem2  31431  cycpmconjs  31432  cyc3conja  31433  smatfval  31754  eulerpartlemgv  32349  eulerpartlemn  32357  eulerpart  32358  sseqval  32364  reprpmtf1o  32615  erdsze2lem2  33175  cvmliftlem10  33265  mrsubval  33480  ftc1anclem8  35866  cocnv  35892  ltrncoidN  38149  trlcoabs2N  38743  cdlemg47a  38755  cdlemg46  38756  cdlemg47  38757  ltrnco4  38760  tendovalco  38786  tendoplcbv  38796  tendopl  38797  tendoplass  38804  cdlemi2  38840  cdlemk2  38853  cdlemk4  38855  cdlemk8  38859  cdlemkuu  38916  cdlemk53  38978  cdlemk54  38979  cdlemk55a  38980  erngdvlem3  39011  erngdvlem3-rN  39019  tendocnv  39042  tendospcanN  39044  dvhvaddcbv  39110  dvhvaddval  39111  dvhvaddass  39118  dvhvscacbv  39119  dvhvscaval  39120  dvhopvsca  39123  dvhlveclem  39129  dvhopspN  39136  diblss  39191  cdlemn8  39225  dihopelvalcpre  39269  dihmeetlem1N  39311  dihglblem5apreN  39312  dih1dimatlem0  39349  dihjatcclem4  39442  diophrw  40588  eldioph2  40591  relexpaddss  41333  trclfvcom  41338  frege131d  41379  fsovrfovd  41624  hoicvrrex  44101  ovnlecvr  44103  ovncvrrp  44109  ovn0lem  44110  ovnsubaddlem1  44115  ovnsubadd  44117  ovnhoilem1  44146  ovnhoi  44148  ovnlecvr2  44155  ovncvr2  44156  hspmbl  44174  ovnovollem1  44201  ovnovollem3  44203