Theorem elpw2g 4588

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 3994	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4571	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3993	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 489	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 472	. . 3 |- ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6	5	expcom 436	. 2 |- ( B e. V -> ( A C_ B -> A e. ~P B ) )
7	1, 6	impbid2 207	1 |- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 187   e. wcel 1870   _Vcvv 3087   C_ wss 3442   ~Pcpw 3985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456  df-pw 3987

This theorem is referenced by:  elpw2  4589  pwnss  4590  knatar  6263  pw2f1olem  7682  fineqvlem  7792  elfir  7935  marypha1  7954  r1sscl  8255  tskwe  8383  dfac8alem  8458  acni2  8475  fin1ai  8721  fin2i  8723  fin23lem7  8744  fin23lem11  8745  isfin2-2  8747  fin23lem39  8778  isf34lem1  8800  isf34lem2  8801  isf34lem4  8805  isf34lem5  8806  fin1a2lem7  8834  fin1a2lem12  8839  canthnumlem  9072  canthp1lem2  9077  wunss  9136  tsken  9178  tskss  9182  gruss  9220  ramub1lem1  14947  ismre  15447  mreintcl  15452  mremre  15461  submre  15462  mrcval  15467  mrccl  15468  mrcun  15479  ismri  15488  mreexd  15499  mreexexlem4d  15504  acsfiel  15511  isacs1i  15514  catcoppccl  15954  acsdrsel  16364  acsdrscl  16367  acsficl  16368  pmtrval  17043  pmtrrn  17049  opsrval  18633  istopg  19856  uniopn  19858  iscld  19973  ntrval  19982  clsval  19983  discld  20036  mretopd  20039  neival  20049  isnei  20050  lpval  20086  restdis  20125  ordtbaslem  20135  ordtuni  20137  cncls  20221  cndis  20238  tgcmp  20347  hauscmplem  20352  comppfsc  20478  elkgen  20482  xkoopn  20535  elqtop  20643  kqffn  20671  isfbas  20775  filss  20799  snfbas  20812  elfg  20817  fbasrn  20830  ufilss  20851  fixufil  20868  cfinufil  20874  ufinffr  20875  ufilen  20876  fin1aufil  20878  rnelfmlem  20898  flimclslem  20930  hauspwpwf1  20933  supnfcls  20966  flimfnfcls  20974  ptcmplem1  20998  tsmsfbas  21073  blfvalps  21329  blfps  21352  blf  21353  bcthlem5  22189  minveclem3b  22263  sigaclcuni  28779  sigaclcu2  28781  pwsiga  28791  erdsze2lem2  29715  cvmsval  29777  cvmsss2  29785  neibastop2lem  30801  tailf  30816  fin2so  31636  sdclem1  31776  elrfirn  35246  elrfirn2  35247  istopclsd  35251  nacsfix  35263  dnnumch1  35608