Theorem elpw2 4601

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 4600	. 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 1823   _Vcvv 3106   C_ wss 3461   ~Pcpw 3999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475  df-pw 4001

This theorem is referenced by:  axpweq  4614  knatar  6228  canth  6229  dffi3  7883  marypha1lem  7885  r1pwss  8193  rankr1bg  8212  pwwf  8216  unwf  8219  rankval2  8227  uniwf  8228  rankpwi  8232  aceq3lem  8492  dfac2a  8501  dfac12lem2  8515  axdc3lem4  8824  axdc4lem  8826  axdclem  8890  grothpw  9193  uzf  11085  ixxf  11542  fzf  11679  incexclem  13730  rpnnen2lem1  14032  rpnnen2lem2  14033  bitsf  14161  sadfval  14186  smufval  14211  smupf  14212  vdwapf  14574  prdsval  14944  prdsds  14953  prdshom  14956  mreacs  15147  acsfn  15148  wunnat  15444  lubeldm  15810  lubval  15813  glbeldm  15823  glbval  15826  clatlem  15940  clatlubcl2  15942  clatglbcl2  15944  issubm  16177  issubg  16400  cntzval  16558  sylow1lem2  16818  lsmvalx  16858  pj1fval  16911  issubrg  17624  islss  17776  lspval  17816  lspcl  17817  islbs  17917  lbsextlem1  17999  lbsextlem3  18001  lbsextlem4  18002  sraval  18017  aspval  18172  ocvfval  18870  ocvval  18871  isobs  18924  islinds  19011  leordtval2  19880  cnpfval  19902  iscnp2  19907  uncmp  20070  cmpfi  20075  cmpfii  20076  2ndc1stc  20118  1stcrest  20120  islly2  20151  hausllycmp  20161  lly1stc  20163  1stckgenlem  20220  xkotf  20252  txlly  20303  txnlly  20304  tx1stc  20317  basqtop  20378  tgqtop  20379  alexsubALTlem3  20715  alexsubALTlem4  20716  alexsubALT  20717  sszcld  21488  cncfval  21558  cnllycmp  21622  bndth  21624  ishtpy  21638  ovolficcss  22047  ovolval  22051  ovolicc2  22099  ismbl  22103  mblsplit  22109  voliunlem3  22128  vitalilem4  22186  vitalilem5  22187  dvfval  22467  dvnfval  22491  cpnfval  22501  plyval  22756  dmarea  23485  wilthlem2  23541  umgrabi  25185  issh  26323  ocval  26396  spanval  26449  hsupval  26450  sshjval  26466  sshjval3  26470  fpwrelmap  27787  sigagensiga  28371  dya2iocuni  28491  coinflippv  28686  ballotlemelo  28690  ballotlem2  28691  ballotth  28740  erdszelem1  28899  kur14lem9  28922  kur14  28924  cnllyscon  28954  elmpst  29160  mclsrcl  29185  mclsval  29187  cover2  30444  cntotbnd  30532  heibor1lem  30545  heibor  30557  isidl  30651  igenval  30698  elmzpcl  30898  eldiophb  30929  rpnnen3  31213  islssfgi  31257  hbt  31320  elmnc  31326  itgoval  31351  itgocn  31354  rgspnval  31358  issubmgm  32849  paddval  35919  pclvalN  36011  polvalN  36026  docavalN  37247  djavalN  37259  dicval  37300  dochval  37475  djhval  37522  lpolconN  37611