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

Theorem pweqi 4580
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 4578 . 2 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
31, 2ax-mp 5 1 𝒫 𝐴 = 𝒫 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  𝒫 cpw 4564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-in 3921  df-ss 3931  df-pw 4566
This theorem is referenced by:  pwfiOLD  9297  rankxplim  9823  pwdju1  10134  fin23lem17  10282  mnfnre  11206  qtopres  23072  hmphdis  23170  ust0  23594  made0  27232  umgrpredgv  28140  issubgr  28268  uhgrissubgr  28272  cusgredg  28421  cffldtocusgr  28444  konigsbergiedgw  29241  shsspwh  30237  circtopn  32482  lfuhgr  33775  rankeq1o  34809  onsucsuccmpi  34968  bj-unirel  35572  elrfi  41064  islmodfg  41443  clsk1indlem4  42408  clsk1indlem1  42409  clsk1independent  42410  omef  44827  caragensplit  44831  caragenelss  44832  carageneld  44833  omeunile  44836  caragensspw  44840  0ome  44860  isomennd  44862  ovn02  44899  lcoop  46582  lincvalsc0  46592  linc0scn0  46594  lincdifsn  46595  linc1  46596  lspsslco  46608  lincresunit3lem2  46651  lincresunit3  46652
  Copyright terms: Public domain W3C validator