Theorem pwidg 3966

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 3453	. 2 |- A C_ A
2		elpwg 3961	. 2 |- ( A e. V -> ( A e. ~P A <-> A C_ A ) )
3	1, 2	mpbiri 237	1 |- ( A e. V -> A e. ~P A )

Syntax hints:   -> wi 4   e. wcel 1889   C_ wss 3406   ~Pcpw 3953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-in 3413  df-ss 3420  df-pw 3955

This theorem is referenced by:  pwid  3967  axpweq  4583  knatar  6253  brwdom2  8093  pwwf  8283  rankpwi  8299  canthp1lem2  9083  canthp1  9084  grothpw  9256  mremre  15522  submre  15523  baspartn  19981  fctop  20031  cctop  20033  ppttop  20034  epttop  20036  isopn3  20094  mretopd  20120  tsmsfbas  21154  gsumesum  28892  esumcst  28896  pwsiga  28964  prsiga  28965  sigainb  28970  pwldsys  28991  ldgenpisyslem1  28997  carsggect  29162  neibastop1  31027  neibastop2lem  31028  topdifinfindis  31761  elrfi  35548  pwssfi  37391  dvnprodlem3  37833  caragenunidm  38339