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

Theorem coeq1d 4861
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
coeq1d  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )

Proof of Theorem coeq1d
StepHypRef Expression
1 coeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 coeq1 4857 . 2  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
31, 2syl 15 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    o. ccom 4709
This theorem is referenced by:  coeq12d  4864  fcof1o  5819  domss2  7036  mapen  7041  mapfien  7415  hashfacen  11408  imasval  13430  cofuass  13779  cofulid  13780  setcinv  13938  catcisolem  13954  catciso  13955  yonedalem3b  14069  gsumvalx  14467  frmdup3  14504  symggrp  14796  gsumval3  15207  gsumzf1o  15212  psrass1lem  16139  coe1add  16357  znval  16505  znle2  16523  dvnfval  19287  evl1sca  19429  evl1var  19431  pf1mpf  19451  pf1ind  19454  hocsubdir  22381  subfacp1lem5  23730  relexpsucr  24041  relexpsucl  24043  relexpcnv  24044  relexpadd  24050  mapmapmap  25251  injsurinj  25252  cmpmorass  26069  cmpidmor2  26072  upixp  26506  f1omvdco2  27494  symggen  27514  psgnunilem1  27519  ltrncoidN  30939  trlcoat  31534  trlcone  31539  cdlemg47a  31545  cdlemg47  31547  ltrnco4  31550  tendovalco  31576  tendoplcbv  31586  tendopl  31587  tendoplass  31594  tendo0pl  31602  tendoipl  31608  cdlemk45  31758  cdlemk53b  31767  cdlemk55a  31770  erngdvlem3  31801  erngdvlem3-rN  31809  tendocnv  31833  dvhvaddcbv  31901  dvhvaddval  31902  dvhvaddass  31909  dicvscacl  32003  cdlemn8  32016  dihordlem7b  32027  dihopelvalcpre  32060
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