Theorem pwid 4564

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  pwnex  7706  r1ordg  9693  rankr1id  9777  cfss  10178  0ram  16982  evl1fval1lem  22305  bastg  22941  fincmp  23368  restlly  23458  ptbasfi  23556  zfbas  23871  ustfilxp  24188  minveclem3b  25405  wilthlem3  27047  coinflipprob  34640  r1wf  35255  mapdunirnN  42110  pwtrrVD  45269  vsetrec  50190