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

Theorem pwidg 4121
Description: Membership of the original in a power set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Assertion
Ref Expression
pwidg (𝐴𝑉𝐴 ∈ 𝒫 𝐴)

Proof of Theorem pwidg
StepHypRef Expression
1 ssid 3587 . 2 𝐴𝐴
2 elpwg 4116 . 2 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐴𝐴𝐴))
31, 2mpbiri 247 1 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wss 3540  𝒫 cpw 4108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110
This theorem is referenced by:  pwid  4122  axpweq  4768  knatar  6507  brwdom2  8361  pwwf  8553  rankpwi  8569  canthp1lem2  9354  canthp1  9355  grothpw  9527  mremre  16087  submre  16088  baspartn  20569  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  isopn3  20680  mretopd  20706  tsmsfbas  21741  gsumesum  29448  esumcst  29452  pwsiga  29520  prsiga  29521  sigainb  29526  pwldsys  29547  ldgenpisyslem1  29553  carsggect  29707  neibastop1  31524  neibastop2lem  31525  topdifinfindis  32370  elrfi  36275  dssmapnvod  37334  ntrk0kbimka  37357  clsk3nimkb  37358  neik0pk1imk0  37365  ntrclscls00  37384  ntrneicls00  37407  pwssfi  38236  dvnprodlem3  38838  caragenunidm  39398
  Copyright terms: Public domain W3C validator