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

Theorem rexlimdvw 2670
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 2666 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  odi  6577  omeulem1  6580  qsss  6720  findcard3  7100  r1pwss  7456  dfac5lem4  7753  climuni  12026  rlimno1  12127  caurcvg2  12150  sscfn1  13694  gsumval2a  14459  gsumval3  15191  opnnei  16857  dislly  17223  txcmplem1  17335  ufileu  17614  alexsubALT  17745  i1faddlem  19048  ulmval  19759  iccllyscon  23781  cvmopnlem  23809  cvmlift2lem10  23843  cvmlift3lem8  23857  iseupa  23881  brbtwn  24527  dffprod  25319  lfinpfin  26303  sdclem2  26452  heibor1lem  26533  elrfi  26769  eldiophb  26836  dnnumch2  27142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator