Theorem pwid 4571

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-pw 4551

This theorem is referenced by:  pwnex  7698  r1ordg  9678  rankr1id  9762  cfss  10163  0ram  16934  evl1fval1lem  22246  bastg  22882  fincmp  23309  restlly  23399  ptbasfi  23497  zfbas  23812  ustfilxp  24129  minveclem3b  25356  wilthlem3  27008  coinflipprob  34514  r1wf  35128  mapdunirnN  41769  pwtrrVD  44941  vsetrec  49828