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

Theorem rexlimdvw 2769
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 2765 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   E.wrex 2643
This theorem is referenced by:  odi  6751  omeulem1  6754  qsss  6894  findcard3  7279  r1pwss  7636  dfac5lem4  7933  climuni  12266  rlimno1  12367  caurcvg2  12391  sscfn1  13937  gsumval2a  14702  gsumval3  15434  opnnei  17100  dislly  17474  txcmplem1  17587  ufileu  17865  alexsubALT  17996  metustel  18463  metustfbas  18470  i1faddlem  19445  ulmval  20156  iseupa  21528  iccllyscon  24709  cvmopnlem  24737  cvmlift2lem10  24771  cvmlift3lem8  24785  brbtwn  25545  lfinpfin  26067  sdclem2  26130  heibor1lem  26202  elrfi  26432  eldiophb  26499  dnnumch2  26804
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 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2647  df-rex 2648
  Copyright terms: Public domain W3C validator