Theorem elpw2g 4323

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 3767	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4309	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3766	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 474	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 457	. . 3 |- ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6	5	expcom 425	. 2 |- ( B e. V -> ( A C_ B -> A e. ~P B ) )
7	1, 6	impbid2 196	1 |- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 177   e. wcel 1721   _Vcvv 2916   C_ wss 3280   ~Pcpw 3759

This theorem is referenced by:  elpw2  4324  pwnss  4325  knatar  6039  pw2f1olem  7171  fineqvlem  7282  elfir  7378  marypha1  7397  r1sscl  7667  tskwe  7793  dfac8alem  7866  acni2  7883  fin1ai  8129  fin2i  8131  fin23lem7  8152  fin23lem11  8153  isfin2-2  8155  fin23lem39  8186  isf34lem1  8208  isf34lem2  8209  isf34lem4  8213  isf34lem5  8214  fin1a2lem7  8242  fin1a2lem12  8247  canthnumlem  8479  canthp1lem2  8484  wunss  8543  tsken  8585  tskss  8589  gruss  8627  ramub1lem1  13349  ismre  13770  mreintcl  13775  mremre  13784  submre  13785  mrcval  13790  mrccl  13791  mrcun  13802  ismri  13811  mreexd  13822  mreexexlem4d  13827  acsfiel  13834  isacs1i  13837  catcoppccl  14218  acsdrsel  14548  acsdrscl  14551  acsficl  14552  opsrval  16490  istopg  16923  uniopn  16925  iscld  17046  ntrval  17055  clsval  17056  discld  17108  mretopd  17111  neival  17121  isnei  17122  lpval  17158  restdis  17196  ordtbaslem  17206  ordtuni  17208  cncls  17292  cndis  17309  tgcmp  17418  hauscmplem  17423  elkgen  17521  xkoopn  17574  elqtop  17682  kqffn  17710  isfbas  17814  filss  17838  snfbas  17851  elfg  17856  fbasrn  17869  ufilss  17890  fixufil  17907  cfinufil  17913  ufinffr  17914  ufilen  17915  fin1aufil  17917  rnelfmlem  17937  flimclslem  17969  hauspwpwf1  17972  supnfcls  18005  flimfnfcls  18013  ptcmplem1  18036  tsmsfbas  18110  blfvalps  18366  blfps  18389  blf  18390  bcthlem5  19234  minveclem3b  19282  sigaclcuni  24454  sigaclcu2  24456  pwsiga  24466  erdsze2lem2  24843  cvmsval  24906  cvmsss2  24914  comppfsc  26277  neibastop2lem  26279  tailf  26294  sdclem1  26337  elrfirn  26639  elrfirn2  26640  istopclsd  26644  nacsfix  26656  dnnumch1  27009  pmtrval  27262  pmtrrn  27267

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761