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

Theorem pwidg 4519
 Description: A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Assertion
Ref Expression
pwidg (𝐴𝑉𝐴 ∈ 𝒫 𝐴)

Proof of Theorem pwidg
StepHypRef Expression
1 ssid 3916 . 2 𝐴𝐴
2 elpwg 4500 . 2 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐴𝐴𝐴))
31, 2mpbiri 261 1 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3860  𝒫 cpw 4497 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-pw 4499 This theorem is referenced by:  pwidb  4520  pwid  4521  axpweq  5236  knatar  7109  brwdom2  9075  pwwf  9274  rankpwi  9290  canthp1lem2  10118  canthp1  10119  mremre  16938  submre  16939  baspartn  21659  fctop  21709  cctop  21711  ppttop  21712  epttop  21714  isopn3  21771  mretopd  21797  tsmsfbas  22833  gsumesum  31550  esumcst  31554  pwsiga  31621  prsiga  31622  sigainb  31627  pwldsys  31648  ldgenpisyslem1  31654  carsggect  31808  ex-sategoelel  32903  neibastop1  34123  neibastop2lem  34124  topdifinfindis  35069  elrfi  40036  dssmapnvod  41122  ntrk0kbimka  41143  clsk3nimkb  41144  neik0pk1imk0  41151  ntrclscls00  41170  ntrneicls00  41193  pwssfi  42080  dvnprodlem3  42984  caragenunidm  43541
 Copyright terms: Public domain W3C validator