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

Theorem pwidg 4559
 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 3993 . 2 𝐴𝐴
2 elpwg 4548 . 2 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐴𝐴𝐴))
31, 2mpbiri 259 1 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3940  𝒫 cpw 4542 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-in 3947  df-ss 3956  df-pw 4544 This theorem is referenced by:  pwidb  4560  pwid  4561  axpweq  5262  knatar  7104  brwdom2  9031  pwwf  9230  rankpwi  9246  canthp1lem2  10069  canthp1  10070  mremre  16870  submre  16871  baspartn  21497  fctop  21547  cctop  21549  ppttop  21550  epttop  21552  isopn3  21609  mretopd  21635  tsmsfbas  22670  gsumesum  31223  esumcst  31227  pwsiga  31294  prsiga  31295  sigainb  31300  pwldsys  31321  ldgenpisyslem1  31327  carsggect  31481  ex-sategoelel  32571  neibastop1  33610  neibastop2lem  33611  topdifinfindis  34515  elrfi  39175  dssmapnvod  40250  ntrk0kbimka  40273  clsk3nimkb  40274  neik0pk1imk0  40281  ntrclscls00  40300  ntrneicls00  40323  pwssfi  41191  dvnprodlem3  42117  caragenunidm  42675
 Copyright terms: Public domain W3C validator