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

Theorem rexlimdvw 2834
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvw.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
rexlimdvw  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimdvw
StepHypRef Expression
1 rexlimdvw.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21a1d 25 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2830 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  odi  7006  omeulem1  7009  qsss  7149  findcard3  7543  r1pwss  7979  dfac5lem4  8284  climuni  13014  rlimno1  13115  caurcvg2  13139  sscfn1  14713  gsumval2a  15492  gsumval3OLD  16362  gsumval3  16365  opnnei  18566  dislly  18943  txcmplem1  19056  ufileu  19334  alexsubALT  19465  metustelOLD  19968  metustel  19969  metustfbasOLD  19982  metustfbas  19983  i1faddlem  21013  ulmval  21730  brbtwn  22968  iseupa  23409  iccllyscon  26987  cvmopnlem  27015  cvmlift2lem10  27049  cvmlift3lem8  27063  lfinpfin  28419  sdclem2  28482  heibor1lem  28552  elrfi  28875  eldiophb  28940  dnnumch2  29243  wwlknredwwlkn0  30205  numclwwlkun  30518
  Copyright terms: Public domain W3C validator