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

Theorem exlimi 1781
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
exlimi.1
exlimi.2
Assertion
Ref Expression
exlimi

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3
2119.23 1777 . 2
3 exlimi.2 . 2
42, 3mpgbi 1543 1
 Colors of variables: wff set class Syntax hints:   wi 6  wex 1537  wnf 1539 This theorem is referenced by:  exlimih  1782  19.41  1799  equs5a  1911  sb5rf  1984  equvin  1999  exlimiv  2023  euan  2170  moexex  2182  ceqsex  2760  sbhypf  2771  vtoclgf  2780  vtoclef  2794  copsexg  4145  copsex2g  4147  reusv2lem1  4426  ralxpf  4737  dmcoss  4851  fv3  5393  tz6.12c  5400  opabiota  6177  zfregcl  7192  scottex  7439  scott0  7440  dfac5lem5  7638  zfcndpow  8118  zfcndreg  8119  zfcndinf  8120  reclem2pr  8552  uzindOLD  9985  mreiincl  13370  exisym1  24037  bnj607  27637  bnj900  27650  dihglblem5  30177 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
 Copyright terms: Public domain W3C validator