Theorem elpw2 4444

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 4443	. 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 1755   _Vcvv 2962   C_ wss 3316   ~Pcpw 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850

This theorem is referenced by:  axpweq  4457  knatar  6035  canth  6036  dffi3  7669  marypha1lem  7671  r1pwss  7979  rankr1bg  7998  pwwf  8002  unwf  8005  rankval2  8013  uniwf  8014  rankpwi  8018  aceq3lem  8278  dfac2a  8287  dfac12lem2  8301  axdc3lem4  8610  axdc4lem  8612  axdclem  8676  grothpw  8980  uzf  10851  ixxf  11297  fzf  11427  incexclem  13281  rpnnen2lem1  13479  rpnnen2lem2  13480  bitsf  13605  sadfval  13630  smufval  13655  smupf  13656  vdwapf  14015  prdsval  14375  prdsds  14384  prdshom  14387  mreacs  14578  acsfn  14579  wunnat  14848  lubeldm  15133  lubval  15136  glbeldm  15146  glbval  15149  clatlem  15263  clatlubcl2  15265  clatglbcl2  15267  issubm  15456  issubg  15660  cntzval  15818  sylow1lem2  16077  lsmvalx  16117  pj1fval  16170  issubrg  16788  islss  16937  lspval  16977  lspcl  16978  islbs  17078  lbsextlem1  17160  lbsextlem3  17162  lbsextlem4  17163  sraval  17178  aspval  17320  ocvfval  17932  ocvval  17933  isobs  17986  islinds  18079  leordtval2  18657  cnpfval  18679  iscnp2  18684  uncmp  18847  cmpfi  18852  cmpfii  18853  2ndc1stc  18896  1stcrest  18898  islly2  18929  hausllycmp  18939  lly1stc  18941  1stckgenlem  18967  xkotf  18999  txlly  19050  txnlly  19051  tx1stc  19064  basqtop  19125  tgqtop  19126  alexsubALTlem3  19462  alexsubALTlem4  19463  alexsubALT  19464  sszcld  20235  cncfval  20305  cnllycmp  20369  bndth  20371  ishtpy  20385  ovolficcss  20794  ovolval  20798  ovolicc2  20846  ismbl  20850  mblsplit  20856  voliunlem3  20874  vitalilem4  20932  vitalilem5  20933  dvfval  21213  dvnfval  21237  cpnfval  21247  plyval  21545  dmarea  22235  wilthlem2  22291  umgrabi  23426  issh  24432  ocval  24505  spanval  24558  hsupval  24559  sshjval  24575  sshjval3  24579  sigagensiga  26437  dya2iocuni  26551  ballotlemelo  26717  ballotlem2  26718  ballotth  26767  erdszelem1  26926  kur14lem9  26949  kur14  26951  cnllyscon  26981  cover2  28448  cntotbnd  28536  heibor1lem  28549  heibor  28561  isidl  28655  igenval  28702  elmzpcl  28904  eldiophb  28937  rpnnen3  29223  islssfgi  29267  hbt  29328  elmnc  29335  itgoval  29360  itgocn  29363  rgspnval  29367  paddval  33012  pclvalN  33104  polvalN  33119  docavalN  34338  djavalN  34350  dicval  34391  dochval  34566  djhval  34613  lpolconN  34702