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

Theorem rexlimdvw 2801
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 2797 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   E.wrex 2675
This theorem is referenced by:  odi  6789  omeulem1  6792  qsss  6932  findcard3  7317  r1pwss  7674  dfac5lem4  7971  climuni  12309  rlimno1  12410  caurcvg2  12434  sscfn1  13980  gsumval2a  14745  gsumval3  15477  opnnei  17147  dislly  17521  txcmplem1  17634  ufileu  17912  alexsubALT  18043  metustelOLD  18542  metustel  18543  metustfbasOLD  18556  metustfbas  18557  i1faddlem  19546  ulmval  20257  iseupa  21648  iccllyscon  24898  cvmopnlem  24926  cvmlift2lem10  24960  cvmlift3lem8  24974  brbtwn  25750  lfinpfin  26281  sdclem2  26344  heibor1lem  26416  elrfi  26646  eldiophb  26713  dnnumch2  27018
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2679  df-rex 2680
  Copyright terms: Public domain W3C validator