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

Theorem rexlimi 2635
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 2583 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 rexlimi.1 . . 3  |-  F/ x ps
43r19.23 2633 . 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 2518   E.wrex 2519
This theorem is referenced by:  rexlimiv  2636  triun  4100  reusv1  4506  reusv3  4514  tfinds  4622  fun11iun  5431  iunfo  8129  iundom2g  8130  fsumcom2  12202  dfon2lem7  23514  rexlimib  24325  bwt2  24959  finminlem  25598
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 2523  df-rex 2524
  Copyright terms: Public domain W3C validator