MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpw2 Unicode version

Theorem elpw2 4356
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
StepHypRef Expression
1 elpw2.1 . 2  |-  B  e. 
_V
2 elpw2g 4355 . 2  |-  ( B  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
31, 2ax-mp 8 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1725   _Vcvv 2948    C_ wss 3312   ~Pcpw 3791
This theorem is referenced by:  axpweq  4368  abexssex  5993  knatar  6071  canth  6530  dffi3  7427  marypha1lem  7429  r1pwss  7699  rankr1bg  7718  pwwf  7722  unwf  7725  rankval2  7733  uniwf  7734  rankpwi  7738  aceq3lem  7990  dfac2a  7999  dfac12lem2  8013  cflim3  8131  cflim2  8132  cfslb  8135  axdc3lem4  8322  axdc4lem  8324  axdclem  8388  grothpw  8690  uzf  10480  ixxf  10915  fzf  11036  incexclem  12604  rpnnen2lem1  12802  rpnnen2lem2  12803  bitsf  12927  sadfval  12952  smufval  12977  smupf  12978  vdwapf  13328  prdsval  13666  prdsds  13674  prdshom  13677  mreacs  13871  acsfn  13872  wunnat  14141  lubval  14424  glbval  14429  clatlem  14527  issubm  14736  issubg  14932  cntzval  15108  sylow1lem2  15221  lsmvalx  15261  pj1fval  15314  issubrg  15856  islss  15999  lspval  16039  lspcl  16040  islbs  16136  lbsextlem1  16218  lbsextlem3  16220  lbsextlem4  16221  sraval  16236  aspval  16375  ocvfval  16881  ocvval  16882  isobs  16935  leordtval2  17264  cnpfval  17286  iscnp2  17291  uncmp  17454  cmpfi  17459  cmpfii  17460  2ndc1stc  17502  1stcrest  17504  islly2  17535  hausllycmp  17545  lly1stc  17547  1stckgenlem  17573  xkotf  17605  txlly  17656  txnlly  17657  tx1stc  17670  basqtop  17731  tgqtop  17732  alexsubALTlem3  18068  alexsubALTlem4  18069  alexsubALT  18070  ustfilxp  18230  sszcld  18836  cncfval  18906  cnllycmp  18969  bndth  18971  ishtpy  18985  ovolficcss  19354  ovolval  19358  ovolicc2  19406  ismbl  19410  mblsplit  19416  voliunlem2  19433  voliunlem3  19434  vitalilem4  19491  vitalilem5  19492  dvfval  19772  dvnfval  19796  cpnfval  19806  plyval  20100  dmarea  20784  wilthlem2  20840  umgrabi  21693  issh  22698  ocval  22770  spanval  22823  hsupval  22824  sshjval  22840  sshjval3  22844  sigagensiga  24512  dya2iocuni  24621  coinflippv  24729  ballotlemelo  24733  ballotlem2  24734  ballotth  24783  erdszelem1  24865  kur14lem9  24888  kur14  24890  cnllyscon  24920  cover2  26352  cntotbnd  26442  heibor1lem  26455  heibor  26467  isidl  26561  igenval  26608  elmzpcl  26720  eldiophb  26752  rpnnen3  27040  islssfgi  27085  islinds  27194  hbt  27249  elmnc  27256  itgoval  27281  itgocn  27284  rgspnval  27288  paddval  30434  pclvalN  30526  polvalN  30541  docavalN  31760  djavalN  31772  dicval  31813  dochval  31988  djhval  32035  lpolconN  32124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-pw 3793
  Copyright terms: Public domain W3C validator