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

Theorem rexlimdvw 2898
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 2893 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   E.wrex 2754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-ral 2758  df-rex 2759
This theorem is referenced by:  odi  7185  omeulem1  7188  qsss  7329  findcard3  7717  r1pwss  8154  dfac5lem4  8459  climuni  13431  rlimno1  13532  caurcvg2  13556  sscfn1  15322  gsumval2a  16122  gsumval3OLD  17124  gsumval3  17127  opnnei  19806  dislly  20182  lfinpfin  20209  txcmplem1  20326  ufileu  20604  alexsubALT  20735  metustelOLD  21238  metustel  21239  metustfbasOLD  21252  metustfbas  21253  i1faddlem  22284  ulmval  22959  brbtwn  24500  wwlknredwwlkn0  25025  iseupa  25263  numclwwlkun  25377  iccllyscon  29428  cvmopnlem  29456  cvmlift2lem10  29490  cvmlift3lem8  29504  sdclem2  31498  heibor1lem  31568  elrfi  34969  eldiophb  35032  dnnumch2  35334
  Copyright terms: Public domain W3C validator