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

Theorem elpw2 4616
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
Hypothesis
Ref Expression
elpw2.1
Assertion
Ref Expression
elpw2

Proof of Theorem elpw2
StepHypRef Expression
1 elpw2.1 . 2
2 elpw2g 4615 . 2
31, 2ax-mp 5 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:  axpweq  4629  knatar  6253  canth  6254  dffi3  7911  marypha1lem  7913  r1pwss  8223  rankr1bg  8242  pwwf  8246  unwf  8249  rankval2  8257  uniwf  8258  rankpwi  8262  aceq3lem  8522  dfac2a  8531  dfac12lem2  8545  axdc3lem4  8854  axdc4lem  8856  axdclem  8920  grothpw  9225  uzf  11113  ixxf  11568  fzf  11705  incexclem  13648  rpnnen2lem1  13948  rpnnen2lem2  13949  bitsf  14077  sadfval  14102  smufval  14127  smupf  14128  vdwapf  14490  prdsval  14852  prdsds  14861  prdshom  14864  mreacs  15055  acsfn  15056  wunnat  15325  lubeldm  15611  lubval  15614  glbeldm  15624  glbval  15627  clatlem  15741  clatlubcl2  15743  clatglbcl2  15745  issubm  15978  issubg  16201  cntzval  16359  sylow1lem2  16619  lsmvalx  16659  pj1fval  16712  issubrg  17429  islss  17581  lspval  17621  lspcl  17622  islbs  17722  lbsextlem1  17804  lbsextlem3  17806  lbsextlem4  17807  sraval  17822  aspval  17977  ocvfval  18697  ocvval  18698  isobs  18751  islinds  18844  leordtval2  19713  cnpfval  19735  iscnp2  19740  uncmp  19903  cmpfi  19908  cmpfii  19909  2ndc1stc  19952  1stcrest  19954  islly2  19985  hausllycmp  19995  lly1stc  19997  1stckgenlem  20054  xkotf  20086  txlly  20137  txnlly  20138  tx1stc  20151  basqtop  20212  tgqtop  20213  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  sszcld  21322  cncfval  21392  cnllycmp  21456  bndth  21458  ishtpy  21472  ovolficcss  21881  ovolval  21885  ovolicc2  21933  ismbl  21937  mblsplit  21943  voliunlem3  21962  vitalilem4  22020  vitalilem5  22021  dvfval  22301  dvnfval  22325  cpnfval  22335  plyval  22590  dmarea  23287  wilthlem2  23343  umgrabi  24983  issh  26125  ocval  26198  spanval  26251  hsupval  26252  sshjval  26268  sshjval3  26272  fpwrelmap  27556  sigagensiga  28141  dya2iocuni  28254  coinflippv  28422  ballotlemelo  28426  ballotlem2  28427  ballotth  28476  erdszelem1  28635  kur14lem9  28658  kur14  28660  cnllyscon  28690  elmpst  28896  mclsrcl  28921  mclsval  28923  cover2  30204  cntotbnd  30292  heibor1lem  30305  heibor  30317  isidl  30411  igenval  30458  elmzpcl  30658  eldiophb  30690  rpnnen3  30974  islssfgi  31018  hbt  31079  elmnc  31085  itgoval  31110  itgocn  31113  rgspnval  31117  issubmgm  32477  paddval  35522  pclvalN  35614  polvalN  35629  docavalN  36850  djavalN  36862  dicval  36903  dochval  37078  djhval  37125  lpolconN  37214
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  ax-sep 4573
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