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

Theorem pweqi 3989
Description: Equality inference for power class. (Contributed by NM, 27-Nov-2013.)
Hypothesis
Ref Expression
pweqi.1  |-  A  =  B
Assertion
Ref Expression
pweqi  |-  ~P A  =  ~P B

Proof of Theorem pweqi
StepHypRef Expression
1 pweqi.1 . 2  |-  A  =  B
2 pweq 3988 . 2  |-  ( A  =  B  ->  ~P A  =  ~P B
)
31, 2ax-mp 5 1  |-  ~P A  =  ~P B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   ~Pcpw 3985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456  df-pw 3987
This theorem is referenced by:  pwfi  7875  rankxplim  8349  pwcda1  8622  fin23lem17  8766  mnfnre  9682  qtopres  20644  hmphdis  20742  ust0  21165  shsspwh  26734  circtopn  28503  rankeq1o  30723  onsucsuccmpi  30888  elrfi  35244  islmodfg  35632  omef  37825  caragensplit  37829  caragenelss  37830  carageneld  37831  omeunile  37834  caragensspw  37838  uhgrepe  38447  lcoop  38963  lincvalsc0  38973  linc0scn0  38975  lincdifsn  38976  linc1  38977  lspsslco  38989  lincresunit3lem2  39032  lincresunit3  39033
  Copyright terms: Public domain W3C validator