Theorem r19.29 2992

Description: Restricted quantifier version of 19.29 1683. See also r19.29r 2993. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
r19.29

Proof of Theorem r19.29

Step	Hyp	Ref	Expression
1		pm3.2 447	. . . 4
2	1	ralimi 2850	. . 3
3		rexim 2922	. . 3
4	2, 3	syl 16	. 2
5	4	imp 429	1

Syntax hints:  ->wi 4  /\wa 369  A.wral 2807  E.wrex 2808

This theorem is referenced by:  r19.29r  2993  r19.29d2r  3000  disjiun  4442  triun  4558  ralxfrd  4666  elrnmptg  5257  fmpt  6052  fliftfun  6210  fun11iun  6760  omabs  7315  findcard3  7783  r1sdom  8213  tcrank  8323  infxpenlem  8412  dfac12k  8548  cfslb2n  8669  cfcoflem  8673  iundom2g  8936  supsrlem  9509  axpre-sup  9567  fimaxre3  10517  limsupbnd2  13306  rlimuni  13373  rlimcld2  13401  rlimno1  13476  pgpfac1lem5  17130  ppttop  19508  epttop  19510  tgcnp  19754  lmcnp  19805  bwth  19910  1stcrest  19954  txlm  20149  tx1stc  20151  fbfinnfr  20342  fbunfip  20370  filuni  20386  ufileu  20420  fbflim2  20478  flftg  20497  ufilcmp  20533  cnpfcf  20542  tsmsxp  20657  metss  21011  lmmbr  21697  ivthlem2  21864  ivthlem3  21865  dyadmax  22007  rhmdvdsr  27808  tpr2rico  27894  esumpcvgval  28084  sigaclcuni  28118  voliune  28201  volfiniune  28202  dya2icoseg2  28249  unirep  30203  heibor1lem  30305  2r19.29  30595  stoweidlem35  31817  ralxfrd2  32303  pmapglbx  35493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813