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

Theorem pweqi 4016
 Description: Equality inference for power class. (Contributed by NM, 27-Nov-2013.)
Hypothesis
Ref Expression
pweqi.1
Assertion
Ref Expression
pweqi

Proof of Theorem pweqi
StepHypRef Expression
1 pweqi.1 . 2
2 pweq 4015 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  ~Pcpw 4012 This theorem is referenced by:  pwfi  7835  rankxplim  8318  pwcda1  8595  fin23lem17  8739  mnfnre  9657  qtopres  20199  hmphdis  20297  ust0  20722  shsspwh  26164  circtopn  27840  rankeq1o  29828  onsucsuccmpi  29908  elrfi  30626  islmodfg  31015  uhgrepe  32378  lcoop  33012  lincvalsc0  33022  linc0scn0  33024  lincdifsn  33025  linc1  33026  lspsslco  33038  lincresunit3lem2  33081  lincresunit3  33082 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-pw 4014
 Copyright terms: Public domain W3C validator