Theorem elpw2 4611

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 4610	. 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 184   e. wcel 1767   _Vcvv 3113   C_ wss 3476   ~Pcpw 4010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012

This theorem is referenced by:  axpweq  4624  knatar  6239  canth  6240  dffi3  7887  marypha1lem  7889  r1pwss  8198  rankr1bg  8217  pwwf  8221  unwf  8224  rankval2  8232  uniwf  8233  rankpwi  8237  aceq3lem  8497  dfac2a  8506  dfac12lem2  8520  axdc3lem4  8829  axdc4lem  8831  axdclem  8895  grothpw  9200  uzf  11081  ixxf  11535  fzf  11672  incexclem  13607  rpnnen2lem1  13805  rpnnen2lem2  13806  bitsf  13932  sadfval  13957  smufval  13982  smupf  13983  vdwapf  14345  prdsval  14706  prdsds  14715  prdshom  14718  mreacs  14909  acsfn  14910  wunnat  15179  lubeldm  15464  lubval  15467  glbeldm  15477  glbval  15480  clatlem  15594  clatlubcl2  15596  clatglbcl2  15598  issubm  15788  issubg  15996  cntzval  16154  sylow1lem2  16415  lsmvalx  16455  pj1fval  16508  issubrg  17212  islss  17364  lspval  17404  lspcl  17405  islbs  17505  lbsextlem1  17587  lbsextlem3  17589  lbsextlem4  17590  sraval  17605  aspval  17748  ocvfval  18464  ocvval  18465  isobs  18518  islinds  18611  leordtval2  19479  cnpfval  19501  iscnp2  19506  uncmp  19669  cmpfi  19674  cmpfii  19675  2ndc1stc  19718  1stcrest  19720  islly2  19751  hausllycmp  19761  lly1stc  19763  1stckgenlem  19789  xkotf  19821  txlly  19872  txnlly  19873  tx1stc  19886  basqtop  19947  tgqtop  19948  alexsubALTlem3  20284  alexsubALTlem4  20285  alexsubALT  20286  sszcld  21057  cncfval  21127  cnllycmp  21191  bndth  21193  ishtpy  21207  ovolficcss  21616  ovolval  21620  ovolicc2  21668  ismbl  21672  mblsplit  21678  voliunlem3  21697  vitalilem4  21755  vitalilem5  21756  dvfval  22036  dvnfval  22060  cpnfval  22070  plyval  22325  dmarea  23015  wilthlem2  23071  umgrabi  24659  issh  25801  ocval  25874  spanval  25927  hsupval  25928  sshjval  25944  sshjval3  25948  sigagensiga  27781  dya2iocuni  27894  ballotlemelo  28066  ballotlem2  28067  ballotth  28116  erdszelem1  28275  kur14lem9  28298  kur14  28300  cnllyscon  28330  cover2  29807  cntotbnd  29895  heibor1lem  29908  heibor  29920  isidl  30014  igenval  30061  elmzpcl  30262  eldiophb  30294  rpnnen3  30578  islssfgi  30622  hbt  30683  elmnc  30690  itgoval  30715  itgocn  30718  rgspnval  30722  paddval  34594  pclvalN  34686  polvalN  34701  docavalN  35920  djavalN  35932  dicval  35973  dochval  36148  djhval  36195  lpolconN  36284