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

Theorem rexlimdvw 2683
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 22 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2679 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  odi  6593  omeulem1  6596  qsss  6736  findcard3  7116  r1pwss  7472  dfac5lem4  7769  climuni  12042  rlimno1  12143  caurcvg2  12166  sscfn1  13710  gsumval2a  14475  gsumval3  15207  opnnei  16873  dislly  17239  txcmplem1  17351  ufileu  17630  alexsubALT  17761  i1faddlem  19064  ulmval  19775  iccllyscon  23796  cvmopnlem  23824  cvmlift2lem10  23858  cvmlift3lem8  23872  iseupa  23896  brbtwn  24599  dffprod  25422  lfinpfin  26406  sdclem2  26555  heibor1lem  26636  elrfi  26872  eldiophb  26939  dnnumch2  27245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator