Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwid Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pwid.1 . 2 𝐴 ∈ V
2 pwidg 4121 . 2 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ 𝒫 𝐴
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator