Theorem elpw2g 4245

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 3660	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4227	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3659	. . . . 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 3651

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 4206

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 3653

This theorem is referenced by:  elpw2  4246  pwnss  4248  ifelpwung  4577  pw2f1odclem  7022  elfir  7174  issubm  13575  issubg  13780  issubrng  14234  issubrg  14256  islssm  14392  islssmg  14393  lspval  14425  lspcl  14426  sraval  14472  istopg  14749  uniopn  14751  iscld  14853  ntrval  14860  clsval  14861  discld  14886  neival  14893  isnei  14894  restdis  14934  cnpfval  14945  cndis  14991  blfvalps  15135  blfps  15159  blf  15160  reldvg  15429  2omap  16652  pw1map  16654