Theorem elpw2g 4219

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)

Assertion

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

Proof of Theorem elpw2g

Step	Hyp	Ref	Expression
1		elpwi 3638	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4202	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3637	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 299	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 282	. . 3 |- ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6	5	expcom 116	. 2 |- ( B e. V -> ( A C_ B -> A e. ~P B ) )
7	1, 6	impbid2 143	1 |- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 105   e. wcel 2180   _Vcvv 2779   C_ wss 3177   ~Pcpw 3629

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-sep 4181

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-v 2781  df-in 3183  df-ss 3190  df-pw 3631

This theorem is referenced by:  elpw2  4220  pwnss  4222  ifelpwung  4549  pw2f1odclem  6963  elfir  7108  issubm  13471  issubg  13676  issubrng  14128  issubrg  14150  islssm  14286  islssmg  14287  lspval  14319  lspcl  14320  sraval  14366  istopg  14638  uniopn  14640  iscld  14742  ntrval  14749  clsval  14750  discld  14775  neival  14782  isnei  14783  restdis  14823  cnpfval  14834  cndis  14880  blfvalps  15024  blfps  15048  blf  15049  reldvg  15318  2omap  16270  pw1map  16272