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

Theorem rexlimi 2622
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 2570 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 rexlimi.1 . . 3  |-  F/ x ps
43r19.23 2620 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
52, 4mpbi 201 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   F/wnf 1539    e. wcel 1621   A.wral 2509   E.wrex 2510
This theorem is referenced by:  rexlimiv  2623  triun  4023  reusv1  4425  reusv3  4433  tfinds  4541  fun11iun  5350  iunfo  8045  iundom2g  8046  fsumcom2  12114  dfon2lem7  23313  rexlimib  24124  bwt2  24758  finminlem  25397
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator