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

Theorem rexlimdvw 2958
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 2953 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  odi  7225  omeulem1  7228  qsss  7369  findcard3  7759  r1pwss  8198  dfac5lem4  8503  climuni  13331  rlimno1  13432  caurcvg2  13456  sscfn1  15040  gsumval2a  15822  gsumval3OLD  16696  gsumval3  16699  opnnei  19384  dislly  19761  txcmplem1  19874  ufileu  20152  alexsubALT  20283  metustelOLD  20786  metustel  20787  metustfbasOLD  20800  metustfbas  20801  i1faddlem  21832  ulmval  22506  brbtwn  23875  wwlknredwwlkn0  24400  iseupa  24638  numclwwlkun  24753  iccllyscon  28332  cvmopnlem  28360  cvmlift2lem10  28394  cvmlift3lem8  28408  lfinpfin  29773  sdclem2  29836  heibor1lem  29906  elrfi  30228  eldiophb  30292  dnnumch2  30595
  Copyright terms: Public domain W3C validator