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

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

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