Theorem elpw2g 4244

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 3659	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4226	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3658	. . . . 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 2200   _Vcvv 2800   C_ wss 3198   ~Pcpw 3650

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-in 3204  df-ss 3211  df-pw 3652

This theorem is referenced by:  elpw2  4245  pwnss  4247  ifelpwung  4576  pw2f1odclem  7015  elfir  7166  issubm  13548  issubg  13753  issubrng  14206  issubrg  14228  islssm  14364  islssmg  14365  lspval  14397  lspcl  14398  sraval  14444  istopg  14716  uniopn  14718  iscld  14820  ntrval  14827  clsval  14828  discld  14853  neival  14860  isnei  14861  restdis  14901  cnpfval  14912  cndis  14958  blfvalps  15102  blfps  15126  blf  15127  reldvg  15396  2omap  16544  pw1map  16546