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

Proof of Theorem rexlimi
StepHypRef Expression
1 rexlimi.2 . . 3
21rgen 2824 . 2
3 rexlimi.1 . . 3
43r19.23 2942 . 2
52, 4mpbi 208 1
 Colors of variables: wff setvar class Syntax hints:   wi 4  wnf 1599   wcel 1767  wral 2814  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