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

Theorem exlimi 1821
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 1819 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1558 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550   F/wnf 1553
This theorem is referenced by:  exlimih  1822  19.41OLD  1901  equs5a  1909  equs5e  1910  equsex  2002  ax12olem3  2007  exdistrf  2062  sbie  2122  sb5rf  2165  euan  2337  moexex  2349  ceqsex  2982  sbhypf  2993  vtoclgf  3002  vtoclef  3016  copsexg  4434  copsex2g  4436  reusv2lem1  4716  ralxpf  5011  dmcoss  5127  fv3  5736  tz6.12c  5742  0neqopab  6111  opabiota  6530  zfregcl  7554  scottex  7801  scott0  7802  dfac5lem5  8000  zfcndpow  8483  zfcndreg  8484  zfcndinf  8485  reclem2pr  8917  uzindOLD  10356  mreiincl  13813  exisym1  26166  eu2ndop1stv  27947  bnj607  29224  bnj900  29237  sb5rfNEW7  29528  dihglblem5  32033
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator