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

Theorem pwid 3639
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 3638 . 2  |-  ( A  e.  _V  ->  A  e.  ~P A )
31, 2ax-mp 10 1  |-  A  e. 
~P A
Colors of variables: wff set class
Syntax hints:    e. wcel 1688   _Vcvv 2789   ~Pcpw 3626
This theorem is referenced by:  r1ordg  7445  rankr1id  7529  cfss  7886  0ram  13061  bastg  16698  fincmp  17114  restlly  17203  ptbasfi  17270  zfbas  17585  minveclem3b  18786  wilthlem3  20302  nZdef  24579  pwtrrVD  27868  pwtrrOLD  27869  mapdunirnN  31107
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-pw 3628
  Copyright terms: Public domain W3C validator