Theorem coeq2d 5863

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

Syntax hints:   → wi 4   = wceq 1542   ∘ ccom 5681

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-co 5686

This theorem is referenced by:  coeq12d  5865  dfpo2  6296  f1ococnv1  6863  funcoeqres  6865  fcof1oinvd  7291  foeqcnvco  7298  f1ofvswap  7304  fparlem3  8100  fparlem4  8101  offsplitfpar  8105  csbwrecsg  8306  mapen  9141  mapfien  9403  wemapwe  9692  hashfacen  14413  hashfacenOLD  14414  s1co  14784  pfxco  14789  relexpsucnnl  14977  relexpsucl  14978  relexpsucld  14981  relexpcnv  14982  relexpaddnn  14998  relexpaddg  15000  prdsval  17401  isofval  17704  cofuass  17839  cofurid  17841  fucid  17924  setcinv  18040  catcisolem  18060  curf2ndf  18200  pwsco2mhm  18714  symggrplem  18765  smndex1igid  18785  f1omvdco2  19316  psgnunilem1  19361  efginvrel2  19595  efginvrel1  19596  vrgpinv  19637  frgpuplem  19640  gsumval3  19775  gsumzf1o  19780  psrass1lemOLD  21493  psrass1lem  21496  mpfrcl  21648  evlsval  21649  selvval  21681  evls1fval  21838  evl1fval  21847  pf1mpf  21871  pf1ind  21874  ofco2  21953  qtophmeo  23321  ustssco  23719  utop2nei  23755  neipcfilu  23801  tngds  24164  tngdsOLD  24165  elovolmr  24993  ovoliunlem3  25021  uniioombllem2  25100  hoddi  31243  fcoinver  31835  fmptco1f1o  31857  fcobij  31947  symgfcoeu  32243  symgcom  32244  tocycf  32276  tocyc01  32277  cycpmconjvlem  32300  cycpmconjv  32301  cycpmconjslem1  32313  cycpmconjslem2  32314  cycpmconjs  32315  cyc3conja  32316  smatfval  32775  eulerpartlemgv  33372  eulerpartlemn  33380  eulerpart  33381  sseqval  33387  reprpmtf1o  33638  erdsze2lem2  34195  cvmliftlem10  34285  mrsubval  34500  ftc1anclem8  36568  cocnv  36593  ltrncoidN  38999  trlcoabs2N  39593  cdlemg47a  39605  cdlemg46  39606  cdlemg47  39607  ltrnco4  39610  tendovalco  39636  tendoplcbv  39646  tendopl  39647  tendoplass  39654  cdlemi2  39690  cdlemk2  39703  cdlemk4  39705  cdlemk8  39709  cdlemkuu  39766  cdlemk53  39828  cdlemk54  39829  cdlemk55a  39830  erngdvlem3  39861  erngdvlem3-rN  39869  tendocnv  39892  tendospcanN  39894  dvhvaddcbv  39960  dvhvaddval  39961  dvhvaddass  39968  dvhvscacbv  39969  dvhvscaval  39970  dvhopvsca  39973  dvhlveclem  39979  dvhopspN  39986  diblss  40041  cdlemn8  40075  dihopelvalcpre  40119  dihmeetlem1N  40161  dihglblem5apreN  40162  dih1dimatlem0  40199  dihjatcclem4  40292  mhmcoaddmpl  41123  rhmcomulmpl  41124  rhmmpl  41125  diophrw  41497  eldioph2  41500  relexpaddss  42469  trclfvcom  42474  frege131d  42515  fsovrfovd  42760  hoicvrrex  45272  ovnlecvr  45274  ovncvrrp  45280  ovn0lem  45281  ovnsubaddlem1  45286  ovnsubadd  45288  ovnhoilem1  45317  ovnhoi  45319  ovnlecvr2  45326  ovncvr2  45327  hspmbl  45345  ovnovollem1  45372  ovnovollem3  45374