Theorem elpw2 4324

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 4323	. 2 |- ( B e. _V -> ( A e. ~P B <-> A C_ B ) )
3	1, 2	ax-mp 8	1 |- ( A e. ~P B <-> A C_ B )

Syntax hints:   <-> wb 177   e. wcel 1721   _Vcvv 2916   C_ wss 3280   ~Pcpw 3759

This theorem is referenced by:  axpweq  4336  abexssex  5961  knatar  6039  canth  6498  dffi3  7394  marypha1lem  7396  r1pwss  7666  rankr1bg  7685  pwwf  7689  unwf  7692  rankval2  7700  uniwf  7701  rankpwi  7705  aceq3lem  7957  dfac2a  7966  dfac12lem2  7980  cflim3  8098  cflim2  8099  cfslb  8102  axdc3lem4  8289  axdc4lem  8291  axdclem  8355  grothpw  8657  uzf  10447  ixxf  10882  fzf  11003  incexclem  12571  rpnnen2lem1  12769  rpnnen2lem2  12770  bitsf  12894  sadfval  12919  smufval  12944  smupf  12945  vdwapf  13295  prdsval  13633  prdsds  13641  prdshom  13644  mreacs  13838  acsfn  13839  wunnat  14108  lubval  14391  glbval  14396  clatlem  14494  issubm  14703  issubg  14899  cntzval  15075  sylow1lem2  15188  lsmvalx  15228  pj1fval  15281  issubrg  15823  islss  15966  lspval  16006  lspcl  16007  islbs  16103  lbsextlem1  16185  lbsextlem3  16187  lbsextlem4  16188  sraval  16203  aspval  16342  ocvfval  16848  ocvval  16849  isobs  16902  leordtval2  17230  cnpfval  17252  iscnp2  17257  uncmp  17420  cmpfi  17425  cmpfii  17426  2ndc1stc  17467  1stcrest  17469  islly2  17500  hausllycmp  17510  lly1stc  17512  1stckgenlem  17538  xkotf  17570  txlly  17621  txnlly  17622  tx1stc  17635  basqtop  17696  tgqtop  17697  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ustfilxp  18195  sszcld  18801  cncfval  18871  cnllycmp  18934  bndth  18936  ishtpy  18950  ovolficcss  19319  ovolval  19323  ovolicc2  19371  ismbl  19375  mblsplit  19381  voliunlem2  19398  voliunlem3  19399  vitalilem4  19456  vitalilem5  19457  dvfval  19737  dvnfval  19761  cpnfval  19771  plyval  20065  dmarea  20749  wilthlem2  20805  umgrabi  21658  issh  22663  ocval  22735  spanval  22788  hsupval  22789  sshjval  22805  sshjval3  22809  sigagensiga  24477  dya2iocuni  24586  coinflippv  24694  ballotlemelo  24698  ballotlem2  24699  ballotth  24748  erdszelem1  24830  kur14lem9  24853  kur14  24855  cnllyscon  24885  cover2  26305  cntotbnd  26395  heibor1lem  26408  heibor  26420  isidl  26514  igenval  26561  elmzpcl  26673  eldiophb  26705  rpnnen3  26993  islssfgi  27038  islinds  27147  hbt  27202  elmnc  27209  itgoval  27234  itgocn  27237  rgspnval  27241  paddval  30280  pclvalN  30372  polvalN  30387  docavalN  31606  djavalN  31618  dicval  31659  dochval  31834  djhval  31881  lpolconN  31970

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761