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
rexlimi.2
Assertion
Ref Expression
rexlimi

Proof of Theorem rexlimi
StepHypRef Expression
1 rexlimi.2 . . 3
21rgen 2783 . 2
3 rexlimi.1 . . 3
43r19.23 2902 . 2
52, 4mpbi 211 1
 Colors of variables: wff setvar class Syntax hints:   wi 4  wnf 1663   wcel 1867  wral 2773  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