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

Theorem coeq1d 5026
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 5022 . 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 1652    o. ccom 4874
This theorem is referenced by:  coeq12d  5029  fcof1o  6018  domss2  7258  mapen  7263  mapfien  7645  hashfacen  11695  imasval  13729  cofuass  14078  cofulid  14079  setcinv  14237  catcisolem  14253  catciso  14254  yonedalem3b  14368  gsumvalx  14766  frmdup3  14803  symggrp  15095  gsumval3  15506  gsumzf1o  15511  psrass1lem  16434  coe1add  16649  znval  16808  znle2  16826  dvnfval  19800  evl1sca  19942  evl1var  19944  pf1mpf  19964  pf1ind  19967  hocsubdir  23280  subfacp1lem5  24862  relexpsucr  25122  relexpsucl  25124  relexpcnv  25125  relexpadd  25130  upixp  26422  f1omvdco2  27359  symggen  27379  psgnunilem1  27384  ltrncoidN  30862  trlcoat  31457  trlcone  31462  cdlemg47a  31468  cdlemg47  31470  ltrnco4  31473  tendovalco  31499  tendoplcbv  31509  tendopl  31510  tendoplass  31517  tendo0pl  31525  tendoipl  31531  cdlemk45  31681  cdlemk53b  31690  cdlemk55a  31693  erngdvlem3  31724  erngdvlem3-rN  31732  tendocnv  31756  dvhvaddcbv  31824  dvhvaddval  31825  dvhvaddass  31832  dicvscacl  31926  cdlemn8  31939  dihordlem7b  31950  dihopelvalcpre  31983
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-in 3319  df-ss 3326  df-br 4205  df-opab 4259  df-co 4879
  Copyright terms: Public domain W3C validator