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

Theorem pwidg 4171
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 3622 . 2 𝐴𝐴
2 elpwg 4164 . 2 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐴𝐴𝐴))
31, 2mpbiri 248 1 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  wss 3572  𝒫 cpw 4156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-in 3579  df-ss 3586  df-pw 4158
This theorem is referenced by:  pwid  4172  axpweq  4840  knatar  6604  brwdom2  8475  pwwf  8667  rankpwi  8683  canthp1lem2  9472  canthp1  9473  grothpw  9645  mremre  16258  submre  16259  baspartn  20752  fctop  20802  cctop  20804  ppttop  20805  epttop  20807  isopn3  20864  mretopd  20890  tsmsfbas  21925  gsumesum  30106  esumcst  30110  pwsiga  30178  prsiga  30179  sigainb  30184  pwldsys  30205  ldgenpisyslem1  30211  carsggect  30365  neibastop1  32338  neibastop2lem  32339  topdifinfindis  33174  elrfi  37083  dssmapnvod  38140  ntrk0kbimka  38163  clsk3nimkb  38164  neik0pk1imk0  38171  ntrclscls00  38190  ntrneicls00  38213  pwssfi  39037  dvnprodlem3  39932  caragenunidm  40491
  Copyright terms: Public domain W3C validator