Theorem elpw2g 4564

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 3951	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4542	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3950	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 495	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 478	. . 3 |- ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6	5	expcom 442	. 2 |- ( B e. V -> ( A C_ B -> A e. ~P B ) )
7	1, 6	impbid2 209	1 |- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 189   e. wcel 1904   _Vcvv 3031   C_ wss 3390   ~Pcpw 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-ss 3404  df-pw 3944

This theorem is referenced by:  elpw2  4565  pwnss  4566  knatar  6266  pw2f1olem  7694  fineqvlem  7804  elfir  7947  marypha1  7966  r1sscl  8274  tskwe  8402  dfac8alem  8478  acni2  8495  fin1ai  8741  fin2i  8743  fin23lem7  8764  fin23lem11  8765  isfin2-2  8767  fin23lem39  8798  isf34lem1  8820  isf34lem2  8821  isf34lem4  8825  isf34lem5  8826  fin1a2lem7  8854  fin1a2lem12  8859  canthnumlem  9091  canthp1lem2  9096  wunss  9155  tsken  9197  tskss  9201  gruss  9239  ramub1lem1  15063  ismre  15574  mreintcl  15579  mremre  15588  submre  15589  mrcval  15594  mrccl  15595  mrcun  15606  ismri  15615  mreexd  15626  mreexexlem4d  15631  acsfiel  15638  isacs1i  15641  catcoppccl  16081  acsdrsel  16491  acsdrscl  16494  acsficl  16495  pmtrval  17170  pmtrrn  17176  opsrval  18775  istopg  20002  uniopn  20004  iscld  20119  ntrval  20128  clsval  20129  discld  20182  mretopd  20185  neival  20195  isnei  20196  lpval  20232  restdis  20271  ordtbaslem  20281  ordtuni  20283  cncls  20367  cndis  20384  tgcmp  20493  hauscmplem  20498  comppfsc  20624  elkgen  20628  xkoopn  20681  elqtop  20789  kqffn  20817  isfbas  20922  filss  20946  snfbas  20959  elfg  20964  fbasrn  20977  ufilss  20998  fixufil  21015  cfinufil  21021  ufinffr  21022  ufilen  21023  fin1aufil  21025  rnelfmlem  21045  flimclslem  21077  hauspwpwf1  21080  supnfcls  21113  flimfnfcls  21121  ptcmplem1  21145  tsmsfbas  21220  blfvalps  21476  blfps  21499  blf  21500  bcthlem5  22374  minveclem3b  22448  minveclem3bOLD  22460  sigaclcuni  29014  sigaclcu2  29016  pwsiga  29026  erdsze2lem2  29999  cvmsval  30061  cvmsss2  30069  neibastop2lem  31087  tailf  31102  fin2so  31996  sdclem1  32136  elrfirn  35608  elrfirn2  35609  istopclsd  35613  nacsfix  35625  dnnumch1  35973  elpwi2  37501