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

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
StepHypRef Expression
1 rexlimdvw.1 . . 3
21a1d 25 . 2
32rexlimdv 2947 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator