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

Theorem elpw2 4175
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 4174 . 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 176    e. wcel 1684   _Vcvv 2788    C_ wss 3152   ~Pcpw 3625
This theorem is referenced by:  axpweq  4187  abexssex  5781  knatar  5857  canth  6294  dffi3  7184  marypha1lem  7186  r1pwss  7456  rankr1bg  7475  pwwf  7479  unwf  7482  rankval2  7490  uniwf  7491  rankpwi  7495  aceq3lem  7747  dfac2a  7756  dfac12lem2  7770  cflim3  7888  cflim2  7889  cfslb  7892  axdc3lem4  8079  axdc4lem  8081  axdclem  8146  grothpw  8448  uzf  10233  ixxf  10666  fzf  10786  incexclem  12295  rpnnen2lem1  12493  rpnnen2lem2  12494  bitsf  12618  sadfval  12643  smufval  12668  smupf  12669  vdwapf  13019  prdsval  13355  prdsds  13363  prdshom  13366  mreacs  13560  acsfn  13561  wunnat  13830  lubval  14113  glbval  14118  clatlem  14216  issubm  14425  issubg  14621  cntzval  14797  sylow1lem2  14910  lsmvalx  14950  pj1fval  15003  issubrg  15545  islss  15692  lspval  15732  lspcl  15733  islbs  15829  lbsextlem1  15911  lbsextlem3  15913  lbsextlem4  15914  sraval  15929  aspval  16068  ocvfval  16566  ocvval  16567  isobs  16620  leordtval2  16942  cnpfval  16964  iscnp2  16969  uncmp  17130  cmpfi  17135  cmpfii  17136  2ndc1stc  17177  1stcrest  17179  islly2  17210  hausllycmp  17220  lly1stc  17222  1stckgenlem  17248  xkotf  17280  txlly  17330  txnlly  17331  tx1stc  17344  basqtop  17402  tgqtop  17403  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  cncfval  18392  cnllycmp  18454  bndth  18456  ishtpy  18470  ovolficcss  18829  ovolval  18833  ovolicc2  18881  ismbl  18885  mblsplit  18891  voliunlem2  18908  voliunlem3  18909  vitalilem4  18966  vitalilem5  18967  dvfval  19247  dvnfval  19271  cpnfval  19281  plyval  19575  dmarea  20252  wilthlem2  20307  issh  21787  ocval  21859  spanval  21912  hsupval  21913  sshjval  21929  sshjval3  21933  erdszelem1  23722  kur14lem9  23745  kur14  23747  cnllyscon  23776  umgrabi  23907  isidlNEW  25446  vtarsuelt  25895  cover2  26358  cntotbnd  26520  heibor1lem  26533  heibor  26545  isidl  26639  igenval  26686  elmzpcl  26804  eldiophb  26836  rpnnen3  27125  islssfgi  27170  islinds  27279  hbt  27334  elmnc  27341  itgoval  27366  itgocn  27369  rgspnval  27373  paddval  29987  pclvalN  30079  polvalN  30094  docavalN  31313  djavalN  31325  dicval  31366  dochval  31541  djhval  31588  lpolconN  31677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator