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

Theorem rexlimdvw 2882
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 26 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2877 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743
This theorem is referenced by:  odi  7280  omeulem1  7283  qsss  7424  findcard3  7814  r1pwss  8255  dfac5lem4  8557  climuni  13616  rlimno1  13717  caurcvg2  13744  sscfn1  15722  gsumval2a  16522  gsumval3  17541  opnnei  20136  dislly  20512  lfinpfin  20539  txcmplem1  20656  ufileu  20934  alexsubALT  21066  metustel  21565  metustfbas  21572  i1faddlem  22651  ulmval  23335  brbtwn  24929  wwlknredwwlkn0  25455  iseupa  25693  numclwwlkun  25807  iccllyscon  29973  cvmopnlem  30001  cvmlift2lem10  30035  cvmlift3lem8  30049  sdclem2  32071  heibor1lem  32141  elrfi  35536  eldiophb  35599  dnnumch2  35903  vtxduhgr0nedg  39546
  Copyright terms: Public domain W3C validator