Theorem elpw2 4580

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)

Hypothesis

Ref	Expression
elpw2.1	|- B e. _V

Assertion

Ref	Expression
elpw2	|- ( A e. ~P B <-> A C_ B )

Proof of Theorem elpw2

Step	Hyp	Ref	Expression
1		elpw2.1	. 2 |- B e. _V
2		elpw2g 4579	. 2 |- ( B e. _V -> ( A e. ~P B <-> A C_ B ) )
3	1, 2	ax-mp 5	1 |- ( A e. ~P B <-> A C_ B )

Syntax hints:   <-> wb 189   e. wcel 1897   _Vcvv 3056   C_ wss 3415   ~Pcpw 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422  df-ss 3429  df-pw 3964

This theorem is referenced by:  axpweq  4593  knatar  6272  canth  6273  dffi3  7970  marypha1lem  7972  r1pwss  8280  rankr1bg  8299  pwwf  8303  unwf  8306  rankval2  8314  uniwf  8315  rankpwi  8319  aceq3lem  8576  dfac2a  8585  dfac12lem2  8599  axdc3lem4  8908  axdc4lem  8910  axdclem  8974  grothpw  9276  uzf  11190  ixxf  11673  fzf  11816  incexclem  13942  rpnnen2lem1  14315  rpnnen2lem2  14316  bitsf  14448  sadfval  14474  smufval  14499  smupf  14500  vdwapf  14970  prdsval  15401  prdsds  15410  prdshom  15413  mreacs  15612  acsfn  15613  wunnat  15909  lubeldm  16275  lubval  16278  glbeldm  16288  glbval  16291  clatlem  16405  clatlubcl2  16407  clatglbcl2  16409  issubm  16642  issubg  16865  cntzval  17023  sylow1lem2  17299  lsmvalx  17339  pj1fval  17392  issubrg  18056  islss  18206  lspval  18246  lspcl  18247  islbs  18347  lbsextlem1  18429  lbsextlem3  18431  lbsextlem4  18432  sraval  18447  aspval  18600  ocvfval  19277  ocvval  19278  isobs  19331  islinds  19415  leordtval2  20276  cnpfval  20298  iscnp2  20303  uncmp  20466  cmpfi  20471  cmpfii  20472  2ndc1stc  20514  1stcrest  20516  islly2  20547  hausllycmp  20557  lly1stc  20559  1stckgenlem  20616  xkotf  20648  txlly  20699  txnlly  20700  tx1stc  20713  basqtop  20774  tgqtop  20775  alexsubALTlem3  21112  alexsubALTlem4  21113  alexsubALT  21114  sszcld  21883  cncfval  21968  cnllycmp  22032  bndth  22034  ishtpy  22051  ovolficcss  22470  ovolval  22474  ovolvalOLD  22475  ovolicc2  22524  ismbl  22528  mblsplit  22534  voliunlem3  22553  vitalilem4  22617  vitalilem5  22618  dvfval  22900  dvnfval  22924  cpnfval  22934  plyval  23195  dmarea  23931  wilthlem2  24042  umgrabi  25759  issh  26909  ocval  26981  spanval  27034  hsupval  27035  sshjval  27051  sshjval3  27055  fpwrelmap  28366  sigagensiga  29011  dya2iocuni  29153  coinflippv  29364  ballotlemelo  29368  ballotlem2  29369  ballotth  29418  ballotthOLD  29456  erdszelem1  29962  kur14lem9  29985  kur14  29987  cnllyscon  30016  elmpst  30222  mclsrcl  30247  mclsval  30249  icoreresf  31799  cover2  32084  cntotbnd  32172  heibor1lem  32185  heibor  32197  isidl  32291  igenval  32338  paddval  33407  pclvalN  33499  polvalN  33514  docavalN  34735  djavalN  34747  dicval  34788  dochval  34963  djhval  35010  lpolconN  35099  elmzpcl  35612  eldiophb  35643  rpnnen3  35931  islssfgi  35974  hbt  36033  elmnc  36039  itgoval  36071  itgocn  36074  rgspnval  36078  issubmgm  40061