Theorem elpw2g 4615

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

Assertion

Ref	Expression
elpw2g

Proof of Theorem elpw2g

Step	Hyp	Ref	Expression
1		elpwi 4021	. 2
2		ssexg 4598	. . . 4
3		elpwg 4020	. . . . 5
4	3	biimparc 487	. . . 4
5	2, 4	syldan 470	. . 3
6	5	expcom 435	. 2
7	1, 6	impbid2 204	1

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

This theorem is referenced by:  elpw2  4616  pwnss  4617  knatar  6253  pw2f1olem  7641  fineqvlem  7754  elfir  7895  marypha1  7914  r1sscl  8224  tskwe  8352  dfac8alem  8431  acni2  8448  fin1ai  8694  fin2i  8696  fin23lem7  8717  fin23lem11  8718  isfin2-2  8720  fin23lem39  8751  isf34lem1  8773  isf34lem2  8774  isf34lem4  8778  isf34lem5  8779  fin1a2lem7  8807  fin1a2lem12  8812  canthnumlem  9047  canthp1lem2  9052  wunss  9111  tsken  9153  tskss  9157  gruss  9195  ramub1lem1  14544  ismre  14987  mreintcl  14992  mremre  15001  submre  15002  mrcval  15007  mrccl  15008  mrcun  15019  ismri  15028  mreexd  15039  mreexexlem4d  15044  acsfiel  15051  isacs1i  15054  catcoppccl  15435  acsdrsel  15797  acsdrscl  15800  acsficl  15801  pmtrval  16476  pmtrrn  16482  opsrval  18139  istopg  19404  uniopn  19406  iscld  19528  ntrval  19537  clsval  19538  discld  19590  mretopd  19593  neival  19603  isnei  19604  lpval  19640  restdis  19679  ordtbaslem  19689  ordtuni  19691  cncls  19775  cndis  19792  tgcmp  19901  hauscmplem  19906  comppfsc  20033  elkgen  20037  xkoopn  20090  elqtop  20198  kqffn  20226  isfbas  20330  filss  20354  snfbas  20367  elfg  20372  fbasrn  20385  ufilss  20406  fixufil  20423  cfinufil  20429  ufinffr  20430  ufilen  20431  fin1aufil  20433  rnelfmlem  20453  flimclslem  20485  hauspwpwf1  20488  supnfcls  20521  flimfnfcls  20529  ptcmplem1  20552  tsmsfbas  20626  blfvalps  20886  blfps  20909  blf  20910  bcthlem5  21767  minveclem3b  21843  sigaclcuni  28118  sigaclcu2  28120  pwsiga  28130  erdsze2lem2  28648  cvmsval  28711  cvmsss2  28719  fin2so  30040  neibastop2lem  30178  tailf  30193  sdclem1  30236  elrfirn  30627  elrfirn2  30628  istopclsd  30632  nacsfix  30644  dnnumch1  30990

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