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

Theorem pwid 3971
Description: A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
pwid.1  |-  A  e. 
_V
Assertion
Ref Expression
pwid  |-  A  e. 
~P A

Proof of Theorem pwid
StepHypRef Expression
1 pwid.1 . 2  |-  A  e. 
_V
2 pwidg 3970 . 2  |-  ( A  e.  _V  ->  A  e.  ~P A )
31, 2ax-mp 5 1  |-  A  e. 
~P A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1844   _Vcvv 3061   ~Pcpw 3957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-in 3423  df-ss 3430  df-pw 3959
This theorem is referenced by:  r1ordg  8230  rankr1id  8314  cfss  8679  0ram  14749  evl1fval1lem  18688  bastg  19761  fincmp  20188  restlly  20278  ptbasfi  20376  zfbas  20691  ustfilxp  21009  metustfbasOLD  21362  metustfbas  21363  minveclem3b  22137  wilthlem3  23727  coinflipprob  28937  mapdunirnN  34683  pwtrrVD  36668
  Copyright terms: Public domain W3C validator