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

Theorem exlimi 1813
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 1809 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1539 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531   F/wnf 1534
This theorem is referenced by:  19.41  1827  equs5a  1840  sb5rf  2043  euan  2213  moexex  2225  ceqsex  2835  sbhypf  2846  vtoclgf  2855  vtoclef  2869  copsexg  4268  copsex2g  4270  reusv2lem1  4551  ralxpf  4846  dmcoss  4960  fv3  5557  tz6.12c  5563  opabiota  6309  zfregcl  7324  scottex  7571  scott0  7572  dfac5lem5  7770  zfcndpow  8254  zfcndreg  8255  zfcndinf  8256  reclem2pr  8688  uzindOLD  10122  mreiincl  13514  exisym1  24935  stoweidlem59  27911  eu2ndop1stv  28083  0neqopab  28192  bnj607  29264  bnj900  29277  sb5rfNEW7  29563  dihglblem5  32110
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator