Theorem elpw2g 4610

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 4019	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4593	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 4018	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 487	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 470	. . 3 |- ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6	5	expcom 435	. 2 |- ( B e. V -> ( A C_ B -> A e. ~P B ) )
7	1, 6	impbid2 204	1 |- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1767   _Vcvv 3113   C_ wss 3476   ~Pcpw 4010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012

This theorem is referenced by:  elpw2  4611  pwnss  4612  knatar  6239  pw2f1olem  7618  fineqvlem  7731  elfir  7871  marypha1  7890  r1sscl  8199  tskwe  8327  dfac8alem  8406  acni2  8423  fin1ai  8669  fin2i  8671  fin23lem7  8692  fin23lem11  8693  isfin2-2  8695  fin23lem39  8726  isf34lem1  8748  isf34lem2  8749  isf34lem4  8753  isf34lem5  8754  fin1a2lem7  8782  fin1a2lem12  8787  canthnumlem  9022  canthp1lem2  9027  wunss  9086  tsken  9128  tskss  9132  gruss  9170  ramub1lem1  14399  ismre  14841  mreintcl  14846  mremre  14855  submre  14856  mrcval  14861  mrccl  14862  mrcun  14873  ismri  14882  mreexd  14893  mreexexlem4d  14898  acsfiel  14905  isacs1i  14908  catcoppccl  15289  acsdrsel  15650  acsdrscl  15653  acsficl  15654  pmtrval  16272  pmtrrn  16278  opsrval  17910  istopg  19171  uniopn  19173  iscld  19294  ntrval  19303  clsval  19304  discld  19356  mretopd  19359  neival  19369  isnei  19370  lpval  19406  restdis  19445  ordtbaslem  19455  ordtuni  19457  cncls  19541  cndis  19558  tgcmp  19667  hauscmplem  19672  elkgen  19772  xkoopn  19825  elqtop  19933  kqffn  19961  isfbas  20065  filss  20089  snfbas  20102  elfg  20107  fbasrn  20120  ufilss  20141  fixufil  20158  cfinufil  20164  ufinffr  20165  ufilen  20166  fin1aufil  20168  rnelfmlem  20188  flimclslem  20220  hauspwpwf1  20223  supnfcls  20256  flimfnfcls  20264  ptcmplem1  20287  tsmsfbas  20361  blfvalps  20621  blfps  20644  blf  20645  bcthlem5  21502  minveclem3b  21578  sigaclcuni  27758  sigaclcu2  27760  pwsiga  27770  erdsze2lem2  28288  cvmsval  28351  cvmsss2  28359  fin2so  29617  comppfsc  29779  neibastop2lem  29781  tailf  29796  sdclem1  29839  elrfirn  30231  elrfirn2  30232  istopclsd  30236  nacsfix  30248  dnnumch1  30594