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

Theorem pwidg 3870
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 3372 . 2  |-  A  C_  A
2 elpwg 3865 . 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 1761    C_ wss 3325   ~Pcpw 3857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332  df-ss 3339  df-pw 3859
This theorem is referenced by:  pwid  3871  axpweq  4466  knatar  6045  brwdom2  7784  pwwf  8010  rankpwi  8026  canthp1lem2  8816  canthp1  8817  grothpw  8989  mremre  14538  submre  14539  baspartn  18459  fctop  18508  cctop  18510  ppttop  18511  epttop  18513  isopn3  18570  mretopd  18596  tsmsfbas  19598  gsumesum  26430  esumcst  26434  pwsiga  26493  prsiga  26494  sigainb  26499  neibastop1  28489  neibastop2lem  28490  elrfi  28939
  Copyright terms: Public domain W3C validator