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

Theorem rexlimdvw 2671
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 2667 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1688   E.wrex 2545
This theorem is referenced by:  odi  6572  omeulem1  6575  qsss  6715  findcard3  7095  r1pwss  7451  dfac5lem4  7748  climuni  12020  rlimno1  12121  caurcvg2  12144  sscfn1  13688  gsumval2a  14453  gsumval3  15185  opnnei  16851  dislly  17217  txcmplem1  17329  ufileu  17608  alexsubALT  17739  i1faddlem  19042  ulmval  19753  iccllyscon  23185  cvmopnlem  23213  cvmlift2lem10  23247  cvmlift3lem8  23261  iseupa  23285  brbtwn  23934  dffprod  24718  lfinpfin  25702  sdclem2  25851  heibor1lem  25932  elrfi  26168  eldiophb  26235  dnnumch2  26541
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1534  df-nf 1537  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator