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

Theorem pwidg 4619
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 4005 . 2 𝐴𝐴
2 elpwg 4602 . 2 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐴𝐴𝐴))
31, 2mpbiri 258 1 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wss 3950  𝒫 cpw 4599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ss 3967  df-pw 4601
This theorem is referenced by:  pwidb  4620  pwid  4621  axpweq  5350  knatar  7378  pwssfi  9218  brwdom2  9614  pwwf  9848  rankpwi  9864  canthp1lem2  10694  canthp1  10695  mremre  17648  submre  17649  baspartn  22962  fctop  23012  cctop  23014  ppttop  23015  epttop  23017  isopn3  23075  mretopd  23101  tsmsfbas  24137  exsslsb  33648  gsumesum  34061  esumcst  34065  pwsiga  34132  prsiga  34133  sigainb  34138  pwldsys  34159  ldgenpisyslem1  34165  carsggect  34321  ex-sategoelel  35427  neibastop1  36361  neibastop2lem  36362  topdifinfindis  37348  elrfi  42710  dssmapnvod  44038  ntrk0kbimka  44057  clsk3nimkb  44058  neik0pk1imk0  44065  ntrclscls00  44084  ntrneicls00  44107  dvnprodlem3  45968  caragenunidm  46528
  Copyright terms: Public domain W3C validator