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

Theorem coeq1d 4845
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 4841 . 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 1623    o. ccom 4693
This theorem is referenced by:  coeq12d  4848  fcof1o  5803  domss2  7020  mapen  7025  mapfien  7399  hashfacen  11392  imasval  13414  cofuass  13763  cofulid  13764  setcinv  13922  catcisolem  13938  catciso  13939  yonedalem3b  14053  gsumvalx  14451  frmdup3  14488  symggrp  14780  gsumval3  15191  gsumzf1o  15196  psrass1lem  16123  coe1add  16341  znval  16489  znle2  16507  dvnfval  19271  evl1sca  19413  evl1var  19415  pf1mpf  19435  pf1ind  19438  hocsubdir  22365  subfacp1lem5  23715  relexpsucr  24026  relexpsucl  24028  relexpcnv  24029  relexpadd  24035  mapmapmap  25148  injsurinj  25149  cmpmorass  25966  cmpidmor2  25969  upixp  26403  f1omvdco2  27391  symggen  27411  psgnunilem1  27416  ltrncoidN  30317  trlcoat  30912  trlcone  30917  cdlemg47a  30923  cdlemg47  30925  ltrnco4  30928  tendovalco  30954  tendoplcbv  30964  tendopl  30965  tendoplass  30972  tendo0pl  30980  tendoipl  30986  cdlemk45  31136  cdlemk53b  31145  cdlemk55a  31148  erngdvlem3  31179  erngdvlem3-rN  31187  tendocnv  31211  dvhvaddcbv  31279  dvhvaddval  31280  dvhvaddass  31287  dicvscacl  31381  cdlemn8  31394  dihordlem7b  31405  dihopelvalcpre  31438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-co 4698
  Copyright terms: Public domain W3C validator