Theorem elpwg 4020

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4615. (Contributed by NM, 6-Aug-2000.)

Assertion

Ref	Expression
elpwg

Proof of Theorem elpwg

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2529	. 2
2		sseq1 3524	. 2
3		selpw 4019	. 2
4	1, 2, 3	vtoclbg 3168	1

Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  C_wss 3475  ~Pcpw 4012

This theorem is referenced by:  elpwi  4021  pwidg  4025  elpwunsn  4070  prsspwg  4187  elpw2g  4615  pwel  4704  f1opw2  6528  eldifpw  6612  elpwun  6613  elpmg  7454  fopwdom  7645  elfpw  7842  f1opwfi  7844  rankwflemb  8232  r1elwf  8235  r1pw  8284  ackbij1lem3  8623  ackbij1lem6  8626  ackbij1lem11  8631  mreexexlemd  15041  acsfn  15056  evls1val  18357  evls1rhm  18359  evls1sca  18360  fiinopn  19410  clsval2  19551  ssntr  19559  neipeltop  19630  nrmsep3  19856  cnrmi  19861  cmpcov  19889  cmpsublem  19899  concompss  19934  kgeni  20038  tgqtop  20213  filss  20354  ufileu  20420  filufint  20421  ustssel  20708  elutop  20736  ustuqtop0  20743  metustssOLD  21056  metustss  21057  metutopOLD  21085  psmetutop  21086  axtgcont1  23865  issubgo  25305  crefi  27850  dispcmp  27862  pcmplfin  27863  indval  28027  isrnsigaOLD  28112  sigaclci  28132  sigainb  28136  elsigagen2  28148  measvunilem  28183  measdivcstOLD  28195  ddeval1  28206  ddeval0  28207  omsfval  28265  limsucncmpi  29910  ismrcd1  30630  dvnprodlem1  31743  dvnprodlem2  31744  stoweidlem50  31832  stoweidlem57  31839  elpwdifsn  32296  gsumlsscl  32976  lincfsuppcl  33014  linccl  33015  lincdifsn  33025  lincellss  33027  ellcoellss  33036  lindslinindsimp1  33058  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  lincresunit3lem2  33081  lincresunit3  33082  elpwgded  33337  snelpwrVD  33631  elpwgdedVD  33717  sspwimpcf  33720  sspwimpcfVD  33721  sspwimpALT2  33728

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