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

Theorem pwid 4622
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 4620 . 2 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ 𝒫 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  Vcvv 3480  𝒫 cpw 4600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-pw 4602
This theorem is referenced by:  pwnex  7779  r1ordg  9818  rankr1id  9902  cfss  10305  0ram  17058  evl1fval1lem  22334  bastg  22973  fincmp  23401  restlly  23491  ptbasfi  23589  zfbas  23904  ustfilxp  24221  minveclem3b  25462  wilthlem3  27113  coinflipprob  34482  mapdunirnN  41652  pwtrrVD  44845  vsetrec  49222
  Copyright terms: Public domain W3C validator