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

Theorem rexlimdvw 2825
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 23 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2821 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  odi  6814  omeulem1  6817  qsss  6957  findcard3  7342  r1pwss  7702  dfac5lem4  7999  climuni  12338  rlimno1  12439  caurcvg2  12463  sscfn1  14009  gsumval2a  14774  gsumval3  15506  opnnei  17176  dislly  17552  txcmplem1  17665  ufileu  17943  alexsubALT  18074  metustelOLD  18573  metustel  18574  metustfbasOLD  18587  metustfbas  18588  i1faddlem  19577  ulmval  20288  iseupa  21679  iccllyscon  24929  cvmopnlem  24957  cvmlift2lem10  24991  cvmlift3lem8  25005  brbtwn  25830  lfinpfin  26374  sdclem2  26437  heibor1lem  26509  elrfi  26739  eldiophb  26806  dnnumch2  27111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator