Theorem pwid 4122

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  r1ordg  8524  rankr1id  8608  cfss  8970  0ram  15562  evl1fval1lem  19515  bastg  20581  fincmp  21006  restlly  21096  ptbasfi  21194  zfbas  21510  ustfilxp  21826  metustfbas  22172  minveclem3b  23007  wilthlem3  24596  coinflipprob  29868  bj-pwnex  32246  mapdunirnN  35957  pwtrrVD  38082  vsetrec  42245