Theorem elpw2g 4247

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 3662	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4229	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3661	. . . . 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 2201   _Vcvv 2801   C_ wss 3199   ~Pcpw 3653

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-sep 4208

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-in 3205  df-ss 3212  df-pw 3655

This theorem is referenced by:  elpw2  4248  if0elpw  4250  pwnss  4251  ifelpwung  4580  pw2f1odclem  7025  elfir  7177  issubm  13578  issubg  13783  issubrng  14237  issubrg  14259  islssm  14395  islssmg  14396  lspval  14428  lspcl  14429  sraval  14475  istopg  14752  uniopn  14754  iscld  14856  ntrval  14863  clsval  14864  discld  14889  neival  14896  isnei  14897  restdis  14937  cnpfval  14948  cndis  14994  blfvalps  15138  blfps  15162  blf  15163  reldvg  15432  2omap  16654  pw1map  16656