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

Theorem pwidg 4330
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 3783 . 2 𝐴𝐴
2 elpwg 4323 . 2 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐴𝐴𝐴))
31, 2mpbiri 249 1 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wss 3732  𝒫 cpw 4315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-in 3739  df-ss 3746  df-pw 4317
This theorem is referenced by:  pwid  4331  axpweq  5000  knatar  6799  brwdom2  8685  pwwf  8885  rankpwi  8901  canthp1lem2  9728  canthp1  9729  grothpw  9901  mremre  16532  submre  16533  baspartn  21038  fctop  21088  cctop  21090  ppttop  21091  epttop  21093  isopn3  21150  mretopd  21176  tsmsfbas  22210  gsumesum  30503  esumcst  30507  pwsiga  30575  prsiga  30576  sigainb  30581  pwldsys  30602  ldgenpisyslem1  30608  carsggect  30762  neibastop1  32729  neibastop2lem  32730  topdifinfindis  33559  elrfi  37867  dssmapnvod  38920  ntrk0kbimka  38943  clsk3nimkb  38944  neik0pk1imk0  38951  ntrclscls00  38970  ntrneicls00  38993  pwssfi  39794  dvnprodlem3  40733  caragenunidm  41294
  Copyright terms: Public domain W3C validator