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

Theorem coeq1d 4975
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 4971 . 2  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    o. ccom 4823
This theorem is referenced by:  coeq12d  4978  fcof1o  5966  domss2  7203  mapen  7208  mapfien  7587  hashfacen  11631  imasval  13665  cofuass  14014  cofulid  14015  setcinv  14173  catcisolem  14189  catciso  14190  yonedalem3b  14304  gsumvalx  14702  frmdup3  14739  symggrp  15031  gsumval3  15442  gsumzf1o  15447  psrass1lem  16370  coe1add  16585  znval  16740  znle2  16758  dvnfval  19676  evl1sca  19818  evl1var  19820  pf1mpf  19840  pf1ind  19843  hocsubdir  23137  subfacp1lem5  24650  relexpsucr  24910  relexpsucl  24912  relexpcnv  24913  relexpadd  24918  upixp  26123  f1omvdco2  27061  symggen  27081  psgnunilem1  27086  ltrncoidN  30243  trlcoat  30838  trlcone  30843  cdlemg47a  30849  cdlemg47  30851  ltrnco4  30854  tendovalco  30880  tendoplcbv  30890  tendopl  30891  tendoplass  30898  tendo0pl  30906  tendoipl  30912  cdlemk45  31062  cdlemk53b  31071  cdlemk55a  31074  erngdvlem3  31105  erngdvlem3-rN  31113  tendocnv  31137  dvhvaddcbv  31205  dvhvaddval  31206  dvhvaddass  31213  dicvscacl  31307  cdlemn8  31320  dihordlem7b  31331  dihopelvalcpre  31364
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-in 3271  df-ss 3278  df-br 4155  df-opab 4209  df-co 4828
  Copyright terms: Public domain W3C validator