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

Theorem pwidg 3885
Description: Membership of the original in a power set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Assertion
Ref Expression
pwidg  |-  ( A  e.  V  ->  A  e.  ~P A )

Proof of Theorem pwidg
StepHypRef Expression
1 ssid 3387 . 2  |-  A  C_  A
2 elpwg 3880 . 2  |-  ( A  e.  V  ->  ( A  e.  ~P A  <->  A 
C_  A ) )
31, 2mpbiri 233 1  |-  ( A  e.  V  ->  A  e.  ~P A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3340   ~Pcpw 3872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2986  df-in 3347  df-ss 3354  df-pw 3874
This theorem is referenced by:  pwid  3886  axpweq  4481  knatar  6060  brwdom2  7800  pwwf  8026  rankpwi  8042  canthp1lem2  8832  canthp1  8833  grothpw  9005  mremre  14554  submre  14555  baspartn  18571  fctop  18620  cctop  18622  ppttop  18623  epttop  18625  isopn3  18682  mretopd  18708  tsmsfbas  19710  gsumesum  26522  esumcst  26526  pwsiga  26585  prsiga  26586  sigainb  26591  neibastop1  28592  neibastop2lem  28593  elrfi  29042
  Copyright terms: Public domain W3C validator