MPE Home 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  |-  F/ x ps
exlimi.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
exlimi  |-  ( E. x ph  ->  ps )

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3  |-  F/ x ps
2119.23 1777 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1543 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537   F/wnf 1539
This theorem is referenced by:  exlimih  1782  19.41  1799  equs5a  1912  sb5rf  1985  equvin  2000  exlimiv  2024  euan  2175  moexex  2187  ceqsex  2797  sbhypf  2808  vtoclgf  2817  vtoclef  2831  copsexg  4224  copsex2g  4226  reusv2lem1  4507  ralxpf  4818  dmcoss  4932  fv3  5474  tz6.12c  5481  opabiota  6259  zfregcl  7276  scottex  7523  scott0  7524  dfac5lem5  7722  zfcndpow  8206  zfcndreg  8207  zfcndinf  8208  reclem2pr  8640  uzindOLD  10073  mreiincl  13460  exisym1  24238  stoweidlem59  27143  bnj607  27997  bnj900  28010  dihglblem5  30655
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