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

Theorem pwid 4165
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 4164 . 2 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ 𝒫 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1988  Vcvv 3195  𝒫 cpw 4149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581  df-pw 4151
This theorem is referenced by:  pwnex  6953  r1ordg  8626  rankr1id  8710  cfss  9072  0ram  15705  evl1fval1lem  19675  bastg  20751  fincmp  21177  restlly  21267  ptbasfi  21365  zfbas  21681  ustfilxp  21997  metustfbas  22343  minveclem3b  23180  wilthlem3  24777  coinflipprob  30515  mapdunirnN  36758  pwtrrVD  38880  vsetrec  42211
  Copyright terms: Public domain W3C validator