Theorem rexlimdvw 2952

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rexlimdvw.1

Assertion

Ref	Expression
rexlimdvw

Distinct variable groups:   ,   ,

Proof of Theorem rexlimdvw

Step	Hyp	Ref	Expression
1		rexlimdvw.1	. . 3
2	1	a1d 25	. 2
3	2	rexlimdv 2947	1

Syntax hints:  ->wi 4  e.wcel 1818  E.wrex 2808

This theorem is referenced by:  odi  7247  omeulem1  7250  qsss  7391  findcard3  7783  r1pwss  8223  dfac5lem4  8528  climuni  13375  rlimno1  13476  caurcvg2  13500  sscfn1  15186  gsumval2a  15906  gsumval3OLD  16908  gsumval3  16911  opnnei  19621  dislly  19998  lfinpfin  20025  txcmplem1  20142  ufileu  20420  alexsubALT  20551  metustelOLD  21054  metustel  21055  metustfbasOLD  21068  metustfbas  21069  i1faddlem  22100  ulmval  22775  brbtwn  24202  wwlknredwwlkn0  24727  iseupa  24965  numclwwlkun  25079  iccllyscon  28695  cvmopnlem  28723  cvmlift2lem10  28757  cvmlift3lem8  28771  sdclem2  30235  heibor1lem  30305  elrfi  30626  eldiophb  30690  dnnumch2  30991

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

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