Theorem elpw2g 4452

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 3866	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4435	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3865	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 484	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 467	. . 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 1761   _Vcvv 2970   C_ wss 3325   ~Pcpw 3857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332  df-ss 3339  df-pw 3859

This theorem is referenced by:  elpw2  4453  pwnss  4454  knatar  6045  pw2f1olem  7411  fineqvlem  7523  elfir  7661  marypha1  7680  r1sscl  7988  tskwe  8116  dfac8alem  8195  acni2  8212  fin1ai  8458  fin2i  8460  fin23lem7  8481  fin23lem11  8482  isfin2-2  8484  fin23lem39  8515  isf34lem1  8537  isf34lem2  8538  isf34lem4  8542  isf34lem5  8543  fin1a2lem7  8571  fin1a2lem12  8576  canthnumlem  8811  canthp1lem2  8816  wunss  8875  tsken  8917  tskss  8921  gruss  8959  ramub1lem1  14083  ismre  14524  mreintcl  14529  mremre  14538  submre  14539  mrcval  14544  mrccl  14545  mrcun  14556  ismri  14565  mreexd  14576  mreexexlem4d  14581  acsfiel  14588  isacs1i  14591  catcoppccl  14972  acsdrsel  15333  acsdrscl  15336  acsficl  15337  pmtrval  15950  pmtrrn  15956  opsrval  17532  istopg  18467  uniopn  18469  iscld  18590  ntrval  18599  clsval  18600  discld  18652  mretopd  18655  neival  18665  isnei  18666  lpval  18702  restdis  18741  ordtbaslem  18751  ordtuni  18753  cncls  18837  cndis  18854  tgcmp  18963  hauscmplem  18968  elkgen  19068  xkoopn  19121  elqtop  19229  kqffn  19257  isfbas  19361  filss  19385  snfbas  19398  elfg  19403  fbasrn  19416  ufilss  19437  fixufil  19454  cfinufil  19460  ufinffr  19461  ufilen  19462  fin1aufil  19464  rnelfmlem  19484  flimclslem  19516  hauspwpwf1  19519  supnfcls  19552  flimfnfcls  19560  ptcmplem1  19583  tsmsfbas  19657  blfvalps  19917  blfps  19940  blf  19941  bcthlem5  20798  minveclem3b  20874  sigaclcuni  26497  sigaclcu2  26499  pwsiga  26509  erdsze2lem2  27022  cvmsval  27085  cvmsss2  27093  fin2so  28341  comppfsc  28504  neibastop2lem  28506  tailf  28521  sdclem1  28564  elrfirn  28956  elrfirn2  28957  istopclsd  28961  nacsfix  28973  dnnumch1  29322