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

Theorem rexlimi 2660
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Hypotheses
Ref Expression
rexlimi.1  |-  F/ x ps
rexlimi.2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
rexlimi  |-  ( E. x  e.  A  ph  ->  ps )

Proof of Theorem rexlimi
StepHypRef Expression
1 rexlimi.2 . . 3  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
21rgen 2608 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 rexlimi.1 . . 3  |-  F/ x ps
43r19.23 2658 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
52, 4mpbi 199 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1531    e. wcel 1684   A.wral 2543   E.wrex 2544
This theorem is referenced by:  rexlimiv  2661  triun  4126  reusv1  4534  reusv3  4542  tfinds  4650  fun11iun  5493  iunfo  8161  iundom2g  8162  fsumcom2  12237  dfon2lem7  24145  rexlimib  24959  bwt2  25592  finminlem  26231  stirlinglem13  27835  stirlinglem14  27836  reuan  27958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator