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

Theorem rexlimi 2905
Description: Restricted quantifier version of exlimi 1967. (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 2783 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 rexlimi.1 . . 3  |-  F/ x ps
43r19.23 2902 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
52, 4mpbi 211 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1663    e. wcel 1867   A.wral 2773   E.wrex 2774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-12 1904
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-ral 2778  df-rex 2779
This theorem is referenced by:  rexlimivOLD  2910  r19.29af2OLD  2965  triun  4524  reusv1  4616  reusv3  4624  tfinds  6691  fun11iun  6758  iunfo  8953  iundom2g  8954  fsumcom2  13802  fprodcom2  14005  dfon2lem7  30263  finminlem  30800  reuan  38049  2zrngmmgm  38761
  Copyright terms: Public domain W3C validator