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

Theorem pwid 4117
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 4116 . 2 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ 𝒫 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1975  Vcvv 3168  𝒫 cpw 4103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-in 3542  df-ss 3549  df-pw 4105
This theorem is referenced by:  r1ordg  8497  rankr1id  8581  cfss  8943  0ram  15504  evl1fval1lem  19457  bastg  20519  fincmp  20944  restlly  21034  ptbasfi  21132  zfbas  21448  ustfilxp  21764  metustfbas  22109  minveclem3b  22920  wilthlem3  24509  coinflipprob  29670  bj-pwnex  32045  mapdunirnN  35756  pwtrrVD  37881
  Copyright terms: Public domain W3C validator