Theorem elpw2g 4460

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 3874	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4443	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 3873	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 487	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 470	. . 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 1756   _Vcvv 2977   C_ wss 3333   ~Pcpw 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340  df-ss 3347  df-pw 3867

This theorem is referenced by:  elpw2  4461  pwnss  4462  knatar  6053  pw2f1olem  7420  fineqvlem  7532  elfir  7670  marypha1  7689  r1sscl  7997  tskwe  8125  dfac8alem  8204  acni2  8221  fin1ai  8467  fin2i  8469  fin23lem7  8490  fin23lem11  8491  isfin2-2  8493  fin23lem39  8524  isf34lem1  8546  isf34lem2  8547  isf34lem4  8551  isf34lem5  8552  fin1a2lem7  8580  fin1a2lem12  8585  canthnumlem  8820  canthp1lem2  8825  wunss  8884  tsken  8926  tskss  8930  gruss  8968  ramub1lem1  14092  ismre  14533  mreintcl  14538  mremre  14547  submre  14548  mrcval  14553  mrccl  14554  mrcun  14565  ismri  14574  mreexd  14585  mreexexlem4d  14590  acsfiel  14597  isacs1i  14600  catcoppccl  14981  acsdrsel  15342  acsdrscl  15345  acsficl  15346  pmtrval  15962  pmtrrn  15968  opsrval  17561  istopg  18513  uniopn  18515  iscld  18636  ntrval  18645  clsval  18646  discld  18698  mretopd  18701  neival  18711  isnei  18712  lpval  18748  restdis  18787  ordtbaslem  18797  ordtuni  18799  cncls  18883  cndis  18900  tgcmp  19009  hauscmplem  19014  elkgen  19114  xkoopn  19167  elqtop  19275  kqffn  19303  isfbas  19407  filss  19431  snfbas  19444  elfg  19449  fbasrn  19462  ufilss  19483  fixufil  19500  cfinufil  19506  ufinffr  19507  ufilen  19508  fin1aufil  19510  rnelfmlem  19530  flimclslem  19562  hauspwpwf1  19565  supnfcls  19598  flimfnfcls  19606  ptcmplem1  19629  tsmsfbas  19703  blfvalps  19963  blfps  19986  blf  19987  bcthlem5  20844  minveclem3b  20920  sigaclcuni  26566  sigaclcu2  26568  pwsiga  26578  erdsze2lem2  27097  cvmsval  27160  cvmsss2  27168  fin2so  28421  comppfsc  28584  neibastop2lem  28586  tailf  28601  sdclem1  28644  elrfirn  29036  elrfirn2  29037  istopclsd  29041  nacsfix  29053  dnnumch1  29402