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

Theorem rexlimi 2660
 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 2608 . 2
3 rexlimi.1 . . 3
43r19.23 2658 . 2
52, 4mpbi 199 1
 Colors of variables: wff set class Syntax hints:   wi 4  wnf 1531   wcel 1684  wral 2543  wrex 2544 This theorem is referenced by:  rexlimiv  2661  triun  4126  reusv1  4534  reusv3  4542  tfinds  4650  fun11iun  5493  iunfo  8161  iundom2g  8162  fsumcom2  12237  dfon2lem7  24145  rexlimib  24959  bwt2  25592  finminlem  26231  stirlinglem13  27835  stirlinglem14  27836  reuan  27958 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
 Copyright terms: Public domain W3C validator