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

Theorem pweqi 4134
 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 4133 . 2 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
31, 2ax-mp 5 1 𝒫 𝐴 = 𝒫 𝐵
 Colors of variables: wff setvar class Syntax hints:   = wceq 1480  𝒫 cpw 4130 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3562  df-ss 3569  df-pw 4132 This theorem is referenced by:  pwfi  8205  rankxplim  8686  pwcda1  8960  fin23lem17  9104  mnfnre  10026  qtopres  21411  hmphdis  21509  ust0  21933  umgrpredgv  25930  issubgr  26056  uhgrissubgr  26060  cusgredg  26207  cffldtocusgr  26230  konigsbergiedgw  26974  konigsbergiedgwOLD  26975  shsspwh  27952  circtopn  29686  rankeq1o  31920  onsucsuccmpi  32084  elrfi  36737  islmodfg  37119  clsk1indlem4  37824  clsk1indlem1  37825  clsk1independent  37826  omef  40017  caragensplit  40021  caragenelss  40022  carageneld  40023  omeunile  40026  caragensspw  40030  0ome  40050  isomennd  40052  ovn02  40089  lcoop  41488  lincvalsc0  41498  linc0scn0  41500  lincdifsn  41501  linc1  41502  lspsslco  41514  lincresunit3lem2  41557  lincresunit3  41558
 Copyright terms: Public domain W3C validator