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

Theorem pwid 3977
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 3976 . 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 1758   _Vcvv 3072   ~Pcpw 3963
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 1954  ax-ext 2431
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 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-v 3074  df-in 3438  df-ss 3445  df-pw 3965
This theorem is referenced by:  r1ordg  8091  rankr1id  8175  cfss  8540  0ram  14194  evl1fval1lem  17884  bastg  18698  fincmp  19123  restlly  19214  ptbasfi  19281  zfbas  19596  ustfilxp  19914  metustfbasOLD  20267  metustfbas  20268  minveclem3b  21042  wilthlem3  22536  coinflipprob  27001  pwtrrVD  31874  mapdunirnN  35614
  Copyright terms: Public domain W3C validator