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

Theorem rexlimdvw 2632
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 24 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2628 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   E.wrex 2510
This theorem is referenced by:  odi  6463  omeulem1  6466  qsss  6606  findcard3  6985  r1pwss  7340  dfac5lem4  7637  climuni  11903  rlimno1  12004  caurcvg2  12027  sscfn1  13538  gsumval2a  14294  gsumval3  15026  opnnei  16689  dislly  17055  txcmplem1  17167  ufileu  17446  alexsubALT  17577  i1faddlem  18880  ulmval  19591  iccllyscon  22952  cvmopnlem  22980  cvmlift2lem10  23014  cvmlift3lem8  23028  iseupa  23052  brbtwn  23701  dffprod  24485  lfinpfin  25469  sdclem2  25618  heibor1lem  25699  elrfi  25935  eldiophb  26002  dnnumch2  26308
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator