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

Theorem rexlimdvw 2641
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 2637 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  odi  6510  omeulem1  6513  qsss  6653  findcard3  7033  r1pwss  7389  dfac5lem4  7686  climuni  11956  rlimno1  12057  caurcvg2  12080  sscfn1  13621  gsumval2a  14386  gsumval3  15118  opnnei  16784  dislly  17150  txcmplem1  17262  ufileu  17541  alexsubALT  17672  i1faddlem  18975  ulmval  19686  iccllyscon  23118  cvmopnlem  23146  cvmlift2lem10  23180  cvmlift3lem8  23194  iseupa  23218  brbtwn  23867  dffprod  24651  lfinpfin  25635  sdclem2  25784  heibor1lem  25865  elrfi  26101  eldiophb  26168  dnnumch2  26474
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 2520  df-rex 2521
  Copyright terms: Public domain W3C validator