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

Theorem rexlimi 2945
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 2824 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 rexlimi.1 . . 3  |-  F/ x ps
43r19.23 2942 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
52, 4mpbi 208 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1599    e. wcel 1767   A.wral 2814   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2819  df-rex 2820
This theorem is referenced by:  rexlimivOLD  2950  r19.29af2  3000  triun  4553  reusv1  4647  reusv3  4655  tfinds  6679  fun11iun  6745  iunfo  8915  iundom2g  8916  fsumcom2  13555  bwthOLD  19717  fprodcom2  28967  dfon2lem7  29074  finminlem  29989  reuan  31879
  Copyright terms: Public domain W3C validator