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

Theorem elpw 4018
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
elpw.1
Assertion
Ref Expression
elpw

Proof of Theorem elpw
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elpw.1 . 2
2 sseq1 3524 . 2
3 df-pw 4014 . 2
41, 2, 3elab2 3249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  e.wcel 1818   cvv 3109  C_wss 3475  ~Pcpw 4012
This theorem is referenced by:  selpw  4019  prsspwOLD  4203  0elpw  4621  snelpwi  4697  snelpw  4698  prelpwi  4699  sspwb  4701  pwssun  4791  xpsspwOLD  5122  knatar  6253  iunpw  6614  ssenen  7711  fissuni  7845  fipreima  7846  fiin  7902  fipwuni  7906  dffi3  7911  marypha1lem  7913  inf3lem6  8071  tz9.12lem3  8228  rankonidlem  8267  r0weon  8411  infpwfien  8464  dfac5lem4  8528  dfac2  8532  dfac12lem2  8545  enfin2i  8722  isfin1-3  8787  itunitc1  8821  hsmexlem4  8830  hsmexlem5  8831  axdc4lem  8856  pwfseqlem1  9057  eltsk2g  9150  ixxssxr  11570  ioof  11651  fzof  11826  hashbclem  12501  incexclem  13648  ramub1lem1  14544  ramub1lem2  14545  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  submrc  15025  isacs2  15050  isssc  15189  homaf  15357  catcfuccl  15436  catcxpccl  15476  clatl  15746  fpwipodrs  15794  isacs4lem  15798  isacs5lem  15799  dprd2dlem1  17090  ablfac1b  17121  cssval  18713  tgdom  19480  distop  19497  fctop  19505  cctop  19507  ppttop  19508  pptbas  19509  epttop  19510  mretopd  19593  resttopon  19662  dishaus  19883  discmp  19898  cmpsublem  19899  cmpsub  19900  bwthOLD  19911  concompid  19932  2ndcsep  19960  cldllycmp  19996  dislly  19998  iskgen3  20050  kgencn2  20058  txuni2  20066  dfac14  20119  prdstopn  20129  txcmplem1  20142  txcmplem2  20143  hmphdis  20297  fbssfi  20338  trfbas2  20344  uffixsn  20426  hauspwpwf1  20488  alexsubALTlem2  20548  met1stc  21024  restmetu  21090  icccmplem1  21327  icccmplem2  21328  opnmbllem  22010  sqff1o  23456  umgra1  24326  uslgra1  24372  usgraedgrnv  24377  usgrarnedg  24384  usgraedg4  24387  usgrares1  24410  cusgrarn  24459  eupath2  24980  sspval  25636  foresf1o  27403  cmpcref  27853  esumpcvgval  28084  esumcvg  28092  pwsiga  28130  difelsiga  28133  sigainb  28136  measssd  28186  cntnevol  28199  ddemeas  28208  mbfmcnt  28239  br2base  28240  sxbrsigalem0  28242  oms0  28266  probun  28358  coinfliprv  28421  ballotth  28476  cvmcov2  28720  elfuns  29565  altxpsspw  29627  elhf2  29832  opnmbllem0  30050  neibastop1  30177  neibastop2lem  30178  heiborlem1  30307  heiborlem8  30314  elrfi  30626  ismrcd2  30631  istopclsd  30632  mrefg2  30639  isnacs3  30642  dfac11  31008  islssfg2  31017  lnr2i  31065  stoweidlem57  31839  prelpw  32299  trsspwALT  33616  trsspwALT2  33617  trsspwALT3  33618  pwtrVD  33624  pclfinN  35624  mapd1o  37375  psshepw  37811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014
  Copyright terms: Public domain W3C validator