Theorem elpw2 4451

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 4450	. 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 1756   _Vcvv 2967   C_ wss 3323   ~Pcpw 3855

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 2419  ax-sep 4408

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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337  df-pw 3857

This theorem is referenced by:  axpweq  4464  knatar  6043  canth  6044  dffi3  7673  marypha1lem  7675  r1pwss  7983  rankr1bg  8002  pwwf  8006  unwf  8009  rankval2  8017  uniwf  8018  rankpwi  8022  aceq3lem  8282  dfac2a  8291  dfac12lem2  8305  axdc3lem4  8614  axdc4lem  8616  axdclem  8680  grothpw  8985  uzf  10856  ixxf  11302  fzf  11433  incexclem  13291  rpnnen2lem1  13489  rpnnen2lem2  13490  bitsf  13615  sadfval  13640  smufval  13665  smupf  13666  vdwapf  14025  prdsval  14385  prdsds  14394  prdshom  14397  mreacs  14588  acsfn  14589  wunnat  14858  lubeldm  15143  lubval  15146  glbeldm  15156  glbval  15159  clatlem  15273  clatlubcl2  15275  clatglbcl2  15277  issubm  15466  issubg  15672  cntzval  15830  sylow1lem2  16089  lsmvalx  16129  pj1fval  16182  issubrg  16845  islss  16996  lspval  17036  lspcl  17037  islbs  17137  lbsextlem1  17219  lbsextlem3  17221  lbsextlem4  17222  sraval  17237  aspval  17379  ocvfval  18071  ocvval  18072  isobs  18125  islinds  18218  leordtval2  18796  cnpfval  18818  iscnp2  18823  uncmp  18986  cmpfi  18991  cmpfii  18992  2ndc1stc  19035  1stcrest  19037  islly2  19068  hausllycmp  19078  lly1stc  19080  1stckgenlem  19106  xkotf  19138  txlly  19189  txnlly  19190  tx1stc  19203  basqtop  19264  tgqtop  19265  alexsubALTlem3  19601  alexsubALTlem4  19602  alexsubALT  19603  sszcld  20374  cncfval  20444  cnllycmp  20508  bndth  20510  ishtpy  20524  ovolficcss  20933  ovolval  20937  ovolicc2  20985  ismbl  20989  mblsplit  20995  voliunlem3  21013  vitalilem4  21071  vitalilem5  21072  dvfval  21352  dvnfval  21376  cpnfval  21386  plyval  21641  dmarea  22331  wilthlem2  22387  umgrabi  23576  issh  24582  ocval  24655  spanval  24708  hsupval  24709  sshjval  24725  sshjval3  24729  sigagensiga  26557  dya2iocuni  26671  ballotlemelo  26843  ballotlem2  26844  ballotth  26893  erdszelem1  27052  kur14lem9  27075  kur14  27077  cnllyscon  27107  cover2  28581  cntotbnd  28669  heibor1lem  28682  heibor  28694  isidl  28788  igenval  28835  elmzpcl  29036  eldiophb  29069  rpnnen3  29355  islssfgi  29399  hbt  29460  elmnc  29467  itgoval  29492  itgocn  29495  rgspnval  29499  paddval  33359  pclvalN  33451  polvalN  33466  docavalN  34685  djavalN  34697  dicval  34738  dochval  34913  djhval  34960  lpolconN  35049