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

Theorem exlimi 1859
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Revised 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 1857 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1604 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1596   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600
This theorem is referenced by:  exlimih  1860  equs5a  1927  equs5e  1928  equsex  2011  nfeqf2  2014  exdistrf  2048  sb5rfOLD  2144  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  moanim  2352  euan  2353  euanOLD  2354  moexex  2371  moexexOLD  2372  2eu6  2393  ceqsex  3154  sbhypf  3165  vtoclgf  3174  vtoclg1f  3175  vtoclef  3191  rspn0  3802  reusv2lem1  4654  copsexg  4738  copsexgOLD  4739  copsex2g  4741  ralxpf  5155  dmcoss  5268  fv3  5885  tz6.12c  5891  opabiota  5937  0neqopab  6336  zfregcl  8032  scottex  8315  scott0  8316  dfac5lem5  8520  zfcndpow  9006  zfcndreg  9007  zfcndinf  9008  reclem2pr  9438  uzindOLD  10967  mreiincl  14868  exisym1  29807  eu2ndop1stv  31988  bnj607  33409  bnj900  33422  bj-equsexv  33750  exlimii  33841  bj-exlimmpi  33914  bj-exlimmpbi  33915  bj-exlimmpbir  33916  dihglblem5  36451
  Copyright terms: Public domain W3C validator