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

Theorem pwidg 4312
 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 3773 . 2 𝐴𝐴
2 elpwg 4305 . 2 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐴𝐴𝐴))
31, 2mpbiri 248 1 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2145   ⊆ wss 3723  𝒫 cpw 4297 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-ss 3737  df-pw 4299 This theorem is referenced by:  pwid  4313  axpweq  4973  knatar  6750  brwdom2  8634  pwwf  8834  rankpwi  8850  canthp1lem2  9677  canthp1  9678  grothpw  9850  mremre  16472  submre  16473  baspartn  20979  fctop  21029  cctop  21031  ppttop  21032  epttop  21034  isopn3  21091  mretopd  21117  tsmsfbas  22151  gsumesum  30461  esumcst  30465  pwsiga  30533  prsiga  30534  sigainb  30539  pwldsys  30560  ldgenpisyslem1  30566  carsggect  30720  neibastop1  32691  neibastop2lem  32692  topdifinfindis  33531  elrfi  37783  dssmapnvod  38840  ntrk0kbimka  38863  clsk3nimkb  38864  neik0pk1imk0  38871  ntrclscls00  38890  ntrneicls00  38913  pwssfi  39732  dvnprodlem3  40681  caragenunidm  41242
 Copyright terms: Public domain W3C validator