Theorem elpw 3572

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 3170	. 2 |- ( x = A -> ( x C_ B <-> A C_ B ) )
3		df-pw 3568	. 2 |- ~P B = { x | x C_ B }
4	1, 2, 3	elab2 2878	1 |- ( A e. ~P B <-> A C_ B )

Syntax hints:   <-> wb 104   e. wcel 2141   _Vcvv 2730   C_ wss 3121   ~Pcpw 3566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134  df-pw 3568

This theorem is referenced by:  velpw  3573  elpwg  3574  prsspw  3752  pwprss  3792  pwtpss  3793  pwv  3795  sspwuni  3957  iinpw  3963  iunpwss  3964  0elpw  4150  pwuni  4178  snelpw  4198  sspwb  4201  ssextss  4205  pwin  4267  pwunss  4268  iunpw  4465  xpsspw  4723  ssenen  6829  pw1ne3  7207  3nsssucpw1  7213  ioof  9928  tgdom  12866  distop  12879  epttop  12884  resttopon  12965  txuni2  13050