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

Theorem elpw2 4064
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 4063 . 2  |-  ( B  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
31, 2ax-mp 10 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1621   _Vcvv 2727    C_ wss 3078   ~Pcpw 3530
This theorem is referenced by:  axpweq  4081  abexssex  5633  knatar  5709  canth  6178  dffi3  7068  marypha1lem  7070  r1pwss  7340  rankr1bg  7359  pwwf  7363  unwf  7366  rankval2  7374  uniwf  7375  rankpwi  7379  aceq3lem  7631  dfac2a  7640  dfac12lem2  7654  cflim3  7772  cflim2  7773  cfslb  7776  axdc3lem4  7963  axdc4lem  7965  axdclem  8030  grothpw  8328  uzf  10112  ixxf  10544  fzf  10664  rpnnen2lem1  12367  rpnnen2lem2  12368  bitsf  12492  sadfval  12517  smufval  12542  smupf  12543  vdwapf  12893  prdsval  13229  prdsds  13237  prdshom  13240  mreacs  13404  acsfn  13405  wunnat  13674  lubval  13957  glbval  13962  clatlem  14060  issubm  14260  issubg  14456  cntzval  14632  sylow1lem2  14745  lsmvalx  14785  pj1fval  14838  issubrg  15380  islss  15527  lspval  15567  lspcl  15568  islbs  15664  lbsextlem1  15743  lbsextlem3  15745  lbsextlem4  15746  sraval  15761  aspval  15900  ocvfval  16398  ocvval  16399  isobs  16452  leordtval2  16774  cnpfval  16796  iscnp2  16801  uncmp  16962  cmpfi  16967  cmpfii  16968  2ndc1stc  17009  1stcrest  17011  islly2  17042  hausllycmp  17052  lly1stc  17054  1stckgenlem  17080  xkotf  17112  txlly  17162  txnlly  17163  tx1stc  17176  basqtop  17234  tgqtop  17235  alexsubALTlem3  17575  alexsubALTlem4  17576  alexsubALT  17577  cncfval  18224  cnllycmp  18286  bndth  18288  ishtpy  18302  ovolficcss  18661  ovolval  18665  ovolicc2  18713  ismbl  18717  mblsplit  18723  voliunlem2  18740  voliunlem3  18741  vitalilem4  18798  vitalilem5  18799  dvfval  19079  dvnfval  19103  cpnfval  19113  plyval  19407  dmarea  20084  wilthlem2  20139  issh  21617  ocval  21689  spanval  21742  hsupval  21743  sshjval  21759  sshjval3  21763  erdszelem1  22893  kur14lem9  22916  kur14  22918  cnllyscon  22947  umgrabi  23078  isidlNEW  24612  vtarsuelt  25061  cover2  25524  cntotbnd  25686  heibor1lem  25699  heibor  25711  isidl  25805  igenval  25852  elmzpcl  25970  eldiophb  26002  rpnnen3  26291  islssfgi  26336  islinds  26445  hbt  26500  elmnc  26507  itgoval  26532  itgocn  26535  rgspnval  26539  paddval  28676  pclvalN  28768  polvalN  28783  docavalN  30002  djavalN  30014  dicval  30055  dochval  30230  djhval  30277  lpolconN  30366
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-pw 3532
  Copyright terms: Public domain W3C validator