Theorem elpw2g 4566

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 3960	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4549	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3959	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 490	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 473	. . 3 |- ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6	5	expcom 437	. 2 |- ( B e. V -> ( A C_ B -> A e. ~P B ) )
7	1, 6	impbid2 208	1 |- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 188   e. wcel 1887   _Vcvv 3045   C_ wss 3404   ~Pcpw 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-ss 3418  df-pw 3953

This theorem is referenced by:  elpw2  4567  pwnss  4568  knatar  6248  pw2f1olem  7676  fineqvlem  7786  elfir  7929  marypha1  7948  r1sscl  8256  tskwe  8384  dfac8alem  8460  acni2  8477  fin1ai  8723  fin2i  8725  fin23lem7  8746  fin23lem11  8747  isfin2-2  8749  fin23lem39  8780  isf34lem1  8802  isf34lem2  8803  isf34lem4  8807  isf34lem5  8808  fin1a2lem7  8836  fin1a2lem12  8841  canthnumlem  9073  canthp1lem2  9078  wunss  9137  tsken  9179  tskss  9183  gruss  9221  ramub1lem1  14984  ismre  15496  mreintcl  15501  mremre  15510  submre  15511  mrcval  15516  mrccl  15517  mrcun  15528  ismri  15537  mreexd  15548  mreexexlem4d  15553  acsfiel  15560  isacs1i  15563  catcoppccl  16003  acsdrsel  16413  acsdrscl  16416  acsficl  16417  pmtrval  17092  pmtrrn  17098  opsrval  18698  istopg  19925  uniopn  19927  iscld  20042  ntrval  20051  clsval  20052  discld  20105  mretopd  20108  neival  20118  isnei  20119  lpval  20155  restdis  20194  ordtbaslem  20204  ordtuni  20206  cncls  20290  cndis  20307  tgcmp  20416  hauscmplem  20421  comppfsc  20547  elkgen  20551  xkoopn  20604  elqtop  20712  kqffn  20740  isfbas  20844  filss  20868  snfbas  20881  elfg  20886  fbasrn  20899  ufilss  20920  fixufil  20937  cfinufil  20943  ufinffr  20944  ufilen  20945  fin1aufil  20947  rnelfmlem  20967  flimclslem  20999  hauspwpwf1  21002  supnfcls  21035  flimfnfcls  21043  ptcmplem1  21067  tsmsfbas  21142  blfvalps  21398  blfps  21421  blf  21422  bcthlem5  22296  minveclem3b  22370  minveclem3bOLD  22382  sigaclcuni  28940  sigaclcu2  28942  pwsiga  28952  erdsze2lem2  29927  cvmsval  29989  cvmsss2  29997  neibastop2lem  31016  tailf  31031  fin2so  31932  sdclem1  32072  elrfirn  35537  elrfirn2  35538  istopclsd  35542  nacsfix  35554  dnnumch1  35902