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

Theorem pweqi 3973
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 3972 . 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 1370   ~Pcpw 3969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3444  df-ss 3451  df-pw 3971
This theorem is referenced by:  pwfi  7718  rankxplim  8198  pwcda1  8475  fin23lem17  8619  mnfnre  9538  qtopres  19404  hmphdis  19502  ust0  19927  shsspwh  24802  rankeq1o  28354  onsucsuccmpi  28434  elrfi  29179  islmodfg  29571  lcoop  31078  lincvalsc0  31088  linc0scn0  31090  lincdifsn  31091  linc1  31092  lspsslco  31104  lincresunit3lem2  31147  lincresunit3  31148
  Copyright terms: Public domain W3C validator