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

Step	Hyp	Ref	Expression
1		ssid 3372	. 2 |- A C_ A
2		elpwg 3865	. 2 |- ( A e. V -> ( A e. ~P A <-> A C_ A ) )
3	1, 2	mpbiri 233	1 |- ( A e. V -> A e. ~P A )

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