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

Theorem elpw 3999
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
elpw.1  |-  A  e. 
_V
Assertion
Ref Expression
elpw  |-  ( A  e.  ~P B  <->  A  C_  B
)

Proof of Theorem elpw
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elpw.1 . 2  |-  A  e. 
_V
2 sseq1 3507 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3995 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3233 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
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
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:  selpw  4000  prsspwOLD  4183  0elpw  4602  snelpwi  4678  snelpw  4679  prelpwi  4680  sspwb  4682  pwssun  4772  xpsspwOLD  5103  knatar  6234  iunpw  6595  ssenen  7689  fissuni  7823  fipreima  7824  fiin  7880  fipwuni  7884  dffi3  7889  marypha1lem  7891  inf3lem6  8048  tz9.12lem3  8205  rankonidlem  8244  r0weon  8388  infpwfien  8441  dfac5lem4  8505  dfac2  8509  dfac12lem2  8522  enfin2i  8699  isfin1-3  8764  itunitc1  8798  hsmexlem4  8807  hsmexlem5  8808  axdc4lem  8833  pwfseqlem1  9034  eltsk2g  9127  ixxssxr  11545  ioof  11626  fzof  11800  hashbclem  12475  incexclem  13622  ramub1lem1  14416  ramub1lem2  14417  prdsplusg  14727  prdsmulr  14728  prdsvsca  14729  submrc  14897  isacs2  14922  isssc  15061  homaf  15226  catcfuccl  15305  catcxpccl  15345  clatl  15615  fpwipodrs  15663  isacs4lem  15667  isacs5lem  15668  dprd2dlem1  16958  ablfac1b  16989  cssval  18580  tgdom  19346  distop  19363  fctop  19371  cctop  19373  ppttop  19374  pptbas  19375  epttop  19376  mretopd  19459  resttopon  19528  dishaus  19749  discmp  19764  cmpsublem  19765  cmpsub  19766  bwthOLD  19777  concompid  19798  2ndcsep  19826  cldllycmp  19862  dislly  19864  iskgen3  19916  kgencn2  19924  txuni2  19932  dfac14  19985  prdstopn  19995  txcmplem1  20008  txcmplem2  20009  hmphdis  20163  fbssfi  20204  trfbas2  20210  uffixsn  20292  hauspwpwf1  20354  alexsubALTlem2  20414  met1stc  20890  restmetu  20956  icccmplem1  21193  icccmplem2  21194  opnmbllem  21876  sqff1o  23321  umgra1  24191  uslgra1  24237  usgraedgrnv  24242  usgrarnedg  24249  usgraedg4  24252  usgrares1  24275  cusgrarn  24324  eupath2  24845  sspval  25501  foresf1o  27268  cmpcref  27719  esumpcvgval  27950  esumcvg  27958  pwsiga  27996  difelsiga  27999  sigainb  28002  measssd  28052  cntnevol  28065  ddemeas  28074  mbfmcnt  28105  br2base  28106  sxbrsigalem0  28108  oms0  28132  probun  28224  coinfliprv  28287  ballotth  28342  cvmcov2  28586  elfuns  29533  altxpsspw  29595  elhf2  29800  opnmbllem0  30018  neibastop1  30145  neibastop2lem  30146  heiborlem1  30275  heiborlem8  30282  elrfi  30594  ismrcd2  30599  istopclsd  30600  mrefg2  30607  isnacs3  30610  dfac11  30976  islssfg2  30985  lnr2i  31033  stoweidlem57  31724  prelpw  32133  trsspwALT  33324  trsspwALT2  33325  trsspwALT3  33326  pwtrVD  33332  pclfinN  35326  mapd1o  37077
  Copyright terms: Public domain W3C validator