Theorem pwid 4583

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	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
pwid	⊢ 𝐴 ∈ 𝒫 𝐴

Proof of Theorem pwid

Step	Hyp	Ref	Expression
1		pwid.1	. 2 ⊢ 𝐴 ∈ V
2		pwidg 4580	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ 𝒫 𝐴

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-pw 4562

This theorem is used by:  pwnex  7762  r1ordg  9764  rankr1id  9848  cfss  10271  0ram  17118  evl1fval1lem  22561  bastg  23197  fincmp  23624  restlly  23715  ptbasfi  23813  zfbas  24128  ustfilxp  24445  minveclem3b  25662  wilthlem3  27314  coinflipprob  34999  r1wf  35611  mapdunirnN  42531  pwtrrVD  45655  vsetrec  50637