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

Theorem rexlimdvw 2948
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 25 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2944 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   E.wrex 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2803  df-rex 2804
This theorem is referenced by:  odi  7127  omeulem1  7130  qsss  7270  findcard3  7665  r1pwss  8101  dfac5lem4  8406  climuni  13147  rlimno1  13248  caurcvg2  13272  sscfn1  14848  gsumval2a  15630  gsumval3OLD  16502  gsumval3  16505  opnnei  18855  dislly  19232  txcmplem1  19345  ufileu  19623  alexsubALT  19754  metustelOLD  20257  metustel  20258  metustfbasOLD  20271  metustfbas  20272  i1faddlem  21303  ulmval  21977  brbtwn  23296  iseupa  23737  iccllyscon  27282  cvmopnlem  27310  cvmlift2lem10  27344  cvmlift3lem8  27358  lfinpfin  28722  sdclem2  28785  heibor1lem  28855  elrfi  29177  eldiophb  29242  dnnumch2  29545  wwlknredwwlkn0  30506  numclwwlkun  30819
  Copyright terms: Public domain W3C validator