Theorem pwid 4590

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 4587	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ 𝒫 𝐴

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  𝒫 cpw 4567

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-pw 4569

This theorem is used by:  pwnex  7767  r1ordg  9760  rankr1id  9844  cfss  10267  0ram  17105  evl1fval1lem  22527  bastg  23160  fincmp  23587  restlly  23677  ptbasfi  23775  zfbas  24090  ustfilxp  24407  minveclem3b  25624  wilthlem3  27271  coinflipprob  34902  r1wf  35514  mapdunirnN  42465  pwtrrVD  45574  vsetrec  50522