Theorem elpw 3607

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)

Hypothesis

Ref	Expression
elpw.1	|- A e. _V

Assertion

Ref	Expression
elpw	|- ( A e. ~P B <-> A C_ B )

Proof of Theorem elpw

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpw.1	. 2 |- A e. _V
2		sseq1 3202	. 2 |- ( x = A -> ( x C_ B <-> A C_ B ) )
3		df-pw 3603	. 2 |- ~P B = { x | x C_ B }
4	1, 2, 3	elab2 2908	1 |- ( A e. ~P B <-> A C_ B )

Syntax hints:   <-> wb 105   e. wcel 2164   _Vcvv 2760   C_ wss 3153   ~Pcpw 3601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3159  df-ss 3166  df-pw 3603

This theorem is referenced by:  velpw  3608  elpwg  3609  prsspw  3791  pwprss  3831  pwtpss  3832  pwv  3834  sspwuni  3997  iinpw  4003  iunpwss  4004  0elpw  4193  pwuni  4221  snelpw  4242  sspwb  4245  ssextss  4249  pwin  4313  pwunss  4314  iunpw  4511  xpsspw  4771  ssenen  6907  pw1ne3  7290  3nsssucpw1  7296  ioof  10037  tgdom  14240  distop  14253  epttop  14258  resttopon  14339  txuni2  14424