Theorem pwidg 4173

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 3624	. 2 |- A C_ A
2		elpwg 4166	. 2 |- ( A e. V -> ( A e. ~P A <-> A C_ A ) )
3	1, 2	mpbiri 248	1 |- ( A e. V -> A e. ~P A )

Syntax hints:   -> wi 4   e. wcel 1990   C_ wss 3574   ~Pcpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  pwid  4174  axpweq  4842  knatar  6607  brwdom2  8478  pwwf  8670  rankpwi  8686  canthp1lem2  9475  canthp1  9476  grothpw  9648  mremre  16264  submre  16265  baspartn  20758  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  isopn3  20870  mretopd  20896  tsmsfbas  21931  gsumesum  30121  esumcst  30125  pwsiga  30193  prsiga  30194  sigainb  30199  pwldsys  30220  ldgenpisyslem1  30226  carsggect  30380  neibastop1  32354  neibastop2lem  32355  topdifinfindis  33194  elrfi  37257  dssmapnvod  38314  ntrk0kbimka  38337  clsk3nimkb  38338  neik0pk1imk0  38345  ntrclscls00  38364  ntrneicls00  38387  pwssfi  39211  dvnprodlem3  40163  caragenunidm  40722