Theorem elpw2 4586

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 4585	. 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 188   e. wcel 1869   _Vcvv 3082   C_ wss 3437   ~Pcpw 3980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444  df-ss 3451  df-pw 3982

This theorem is referenced by:  axpweq  4599  knatar  6261  canth  6262  dffi3  7949  marypha1lem  7951  r1pwss  8258  rankr1bg  8277  pwwf  8281  unwf  8284  rankval2  8292  uniwf  8293  rankpwi  8297  aceq3lem  8553  dfac2a  8562  dfac12lem2  8576  axdc3lem4  8885  axdc4lem  8887  axdclem  8951  grothpw  9253  uzf  11164  ixxf  11647  fzf  11790  incexclem  13887  rpnnen2lem1  14260  rpnnen2lem2  14261  bitsf  14393  sadfval  14419  smufval  14444  smupf  14445  vdwapf  14915  prdsval  15346  prdsds  15355  prdshom  15358  mreacs  15557  acsfn  15558  wunnat  15854  lubeldm  16220  lubval  16223  glbeldm  16233  glbval  16236  clatlem  16350  clatlubcl2  16352  clatglbcl2  16354  issubm  16587  issubg  16810  cntzval  16968  sylow1lem2  17244  lsmvalx  17284  pj1fval  17337  issubrg  18001  islss  18151  lspval  18191  lspcl  18192  islbs  18292  lbsextlem1  18374  lbsextlem3  18376  lbsextlem4  18377  sraval  18392  aspval  18545  ocvfval  19221  ocvval  19222  isobs  19275  islinds  19359  leordtval2  20220  cnpfval  20242  iscnp2  20247  uncmp  20410  cmpfi  20415  cmpfii  20416  2ndc1stc  20458  1stcrest  20460  islly2  20491  hausllycmp  20501  lly1stc  20503  1stckgenlem  20560  xkotf  20592  txlly  20643  txnlly  20644  tx1stc  20657  basqtop  20718  tgqtop  20719  alexsubALTlem3  21056  alexsubALTlem4  21057  alexsubALT  21058  sszcld  21827  cncfval  21912  cnllycmp  21976  bndth  21978  ishtpy  21995  ovolficcss  22414  ovolval  22418  ovolvalOLD  22419  ovolicc2  22468  ismbl  22472  mblsplit  22478  voliunlem3  22497  vitalilem4  22561  vitalilem5  22562  dvfval  22844  dvnfval  22868  cpnfval  22878  plyval  23139  dmarea  23875  wilthlem2  23986  umgrabi  25703  issh  26853  ocval  26925  spanval  26978  hsupval  26979  sshjval  26995  sshjval3  26999  fpwrelmap  28318  sigagensiga  28965  dya2iocuni  29107  coinflippv  29318  ballotlemelo  29322  ballotlem2  29323  ballotth  29372  ballotthOLD  29410  erdszelem1  29916  kur14lem9  29939  kur14  29941  cnllyscon  29970  elmpst  30176  mclsrcl  30201  mclsval  30203  icoreresf  31713  cover2  31998  cntotbnd  32086  heibor1lem  32099  heibor  32111  isidl  32205  igenval  32252  paddval  33326  pclvalN  33418  polvalN  33433  docavalN  34654  djavalN  34666  dicval  34707  dochval  34882  djhval  34929  lpolconN  35018  elmzpcl  35531  eldiophb  35562  rpnnen3  35851  islssfgi  35894  hbt  35953  elmnc  35959  itgoval  35991  itgocn  35994  rgspnval  35998  issubmgm  39131