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

Theorem pwid 4365
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 4364 . 2 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ 𝒫 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  Vcvv 3385  𝒫 cpw 4349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-in 3776  df-ss 3783  df-pw 4351
This theorem is referenced by:  pwnex  7201  r1ordg  8891  rankr1id  8975  cfss  9375  0ram  16057  evl1fval1lem  20016  bastg  21099  fincmp  21525  restlly  21615  ptbasfi  21713  zfbas  22028  ustfilxp  22344  minveclem3b  23538  wilthlem3  25148  coinflipprob  31058  mapdunirnN  37671  pwtrrVD  39821  vsetrec  43248
  Copyright terms: Public domain W3C validator