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

Theorem rexlimdvw 2839
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 2835 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716
This theorem is referenced by:  odi  7010  omeulem1  7013  qsss  7153  findcard3  7547  r1pwss  7983  dfac5lem4  8288  climuni  13022  rlimno1  13123  caurcvg2  13147  sscfn1  14722  gsumval2a  15503  gsumval3OLD  16373  gsumval3  16376  opnnei  18699  dislly  19076  txcmplem1  19189  ufileu  19467  alexsubALT  19598  metustelOLD  20101  metustel  20102  metustfbasOLD  20115  metustfbas  20116  i1faddlem  21146  ulmval  21820  brbtwn  23096  iseupa  23537  iccllyscon  27091  cvmopnlem  27119  cvmlift2lem10  27153  cvmlift3lem8  27167  lfinpfin  28528  sdclem2  28591  heibor1lem  28661  elrfi  28983  eldiophb  29048  dnnumch2  29351  wwlknredwwlkn0  30312  numclwwlkun  30625
  Copyright terms: Public domain W3C validator