MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coeq2d Unicode version

Theorem coeq2d 4862
Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
Hypothesis
Ref Expression
coeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
coeq2d  |-  ( ph  ->  ( C  o.  A
)  =  ( C  o.  B ) )

Proof of Theorem coeq2d
StepHypRef Expression
1 coeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 coeq2 4858 . 2  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C  o.  A
)  =  ( C  o.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    o. ccom 4709
This theorem is referenced by:  coeq12d  4864  relcoi1  5217  f1ococnv1  5518  funcoeqres  5520  fcof1o  5819  foeqcnvco  5820  fparlem3  6236  fparlem4  6237  mapen  7041  mapfien  7415  wemapwe  7416  hashfacen  11408  s1co  11504  prdsval  13371  isoval  13683  cofuass  13779  cofurid  13781  fucid  13861  setcinv  13938  catcisolem  13954  curf2ndf  14037  pwsco2mhm  14463  symggrp  14796  efginvrel2  15052  efginvrel1  15053  vrgpinv  15094  frgpuplem  15097  gsumval3  15207  gsumzf1o  15212  psrass1lem  16139  qtophmeo  17524  tngds  18180  elovolmr  18851  ovoliunlem3  18879  uniioombllem2  18954  mpfrcl  19418  evlsval  19419  evl1fval  19426  pf1mpf  19451  pf1ind  19454  hoddi  22586  erdsze2lem2  23750  cvmliftlem10  23840  relexpsucl  24043  relexpadd  24050  dfpo2  24183  valcurfn1  25307  cmpmorass  26069  cmpidmor3  26073  cocnv  26496  diophrw  26941  eldioph2  26944  f1omvdco2  27494  psgnunilem1  27519  ltrncoidN  30939  trlcoabs2N  31533  cdlemg47a  31545  cdlemg46  31546  cdlemg47  31547  ltrnco4  31550  tendovalco  31576  tendoplcbv  31586  tendopl  31587  tendoplass  31594  cdlemi2  31630  cdlemk2  31643  cdlemk4  31645  cdlemk8  31649  cdlemkuu  31706  cdlemk53  31768  cdlemk54  31769  cdlemk55a  31770  erngdvlem3  31801  erngdvlem3-rN  31809  tendocnv  31833  tendospcanN  31835  dvhvaddcbv  31901  dvhvaddval  31902  dvhvaddass  31909  dvhvscacbv  31910  dvhvscaval  31911  dvhopvsca  31914  dvhlveclem  31920  dvhopspN  31927  diblss  31982  cdlemn8  32016  dihopelvalcpre  32060  dihmeetlem1N  32102  dihglblem5apreN  32103  dih1dimatlem0  32140  dihjatcclem4  32233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-br 4040  df-opab 4094  df-co 4714
  Copyright terms: Public domain W3C validator