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

Step	Hyp	Ref	Expression
1		pwid.1	. 2 |- A e. _V
2		pwidg 3976	. 2 |- ( A e. _V -> A e. ~P A )
3	1, 2	ax-mp 5	1 |- A e. ~P A

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