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

Step	Hyp	Ref	Expression
1		ssid 3387	. 2 |- A C_ A
2		elpwg 3880	. 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 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