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

Theorem exlimi 1802
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 1798 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1537 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1529   F/wnf 1532
This theorem is referenced by:  19.41  1816  equs5a  1829  sb5rf  2029  euan  2201  moexex  2213  ceqsex  2823  sbhypf  2834  vtoclgf  2843  vtoclef  2857  copsexg  4251  copsex2g  4253  reusv2lem1  4534  ralxpf  4829  dmcoss  4943  fv3  5501  tz6.12c  5508  opabiota  6286  zfregcl  7303  scottex  7550  scott0  7551  dfac5lem5  7749  zfcndpow  8233  zfcndreg  8234  zfcndinf  8235  reclem2pr  8667  uzindOLD  10101  mreiincl  13492  exisym1  24270  stoweidlem59  27207  bnj607  28215  bnj900  28228  dihglblem5  30755
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533
  Copyright terms: Public domain W3C validator