Theorem elpw2 4597

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 4596	. 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 1802   _Vcvv 3093   C_ wss 3458   ~Pcpw 3993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465  df-ss 3472  df-pw 3995

This theorem is referenced by:  axpweq  4610  knatar  6234  canth  6235  dffi3  7889  marypha1lem  7891  r1pwss  8200  rankr1bg  8219  pwwf  8223  unwf  8226  rankval2  8234  uniwf  8235  rankpwi  8239  aceq3lem  8499  dfac2a  8508  dfac12lem2  8522  axdc3lem4  8831  axdc4lem  8833  axdclem  8897  grothpw  9202  uzf  11088  ixxf  11543  fzf  11680  incexclem  13622  rpnnen2lem1  13820  rpnnen2lem2  13821  bitsf  13949  sadfval  13974  smufval  13999  smupf  14000  vdwapf  14362  prdsval  14724  prdsds  14733  prdshom  14736  mreacs  14927  acsfn  14928  wunnat  15194  lubeldm  15480  lubval  15483  glbeldm  15493  glbval  15496  clatlem  15610  clatlubcl2  15612  clatglbcl2  15614  issubm  15847  issubg  16070  cntzval  16228  sylow1lem2  16488  lsmvalx  16528  pj1fval  16581  issubrg  17297  islss  17449  lspval  17489  lspcl  17490  islbs  17590  lbsextlem1  17672  lbsextlem3  17674  lbsextlem4  17675  sraval  17690  aspval  17845  ocvfval  18564  ocvval  18565  isobs  18618  islinds  18711  leordtval2  19579  cnpfval  19601  iscnp2  19606  uncmp  19769  cmpfi  19774  cmpfii  19775  2ndc1stc  19818  1stcrest  19820  islly2  19851  hausllycmp  19861  lly1stc  19863  1stckgenlem  19920  xkotf  19952  txlly  20003  txnlly  20004  tx1stc  20017  basqtop  20078  tgqtop  20079  alexsubALTlem3  20415  alexsubALTlem4  20416  alexsubALT  20417  sszcld  21188  cncfval  21258  cnllycmp  21322  bndth  21324  ishtpy  21338  ovolficcss  21747  ovolval  21751  ovolicc2  21799  ismbl  21803  mblsplit  21809  voliunlem3  21828  vitalilem4  21886  vitalilem5  21887  dvfval  22167  dvnfval  22191  cpnfval  22201  plyval  22456  dmarea  23152  wilthlem2  23208  umgrabi  24848  issh  25990  ocval  26063  spanval  26116  hsupval  26117  sshjval  26133  sshjval3  26137  fpwrelmap  27421  sigagensiga  28007  dya2iocuni  28120  coinflippv  28288  ballotlemelo  28292  ballotlem2  28293  ballotth  28342  erdszelem1  28501  kur14lem9  28524  kur14  28526  cnllyscon  28556  elmpst  28762  mclsrcl  28787  mclsval  28789  cover2  30172  cntotbnd  30260  heibor1lem  30273  heibor  30285  isidl  30379  igenval  30426  elmzpcl  30626  eldiophb  30658  rpnnen3  30942  islssfgi  30986  hbt  31047  elmnc  31054  itgoval  31079  itgocn  31082  rgspnval  31086  issubmgm  32311  paddval  35224  pclvalN  35316  polvalN  35331  docavalN  36552  djavalN  36564  dicval  36605  dochval  36780  djhval  36827  lpolconN  36916