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

Theorem exlimi 1850
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 1848 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1595 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1587   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  exlimih  1851  equs5a  1918  equs5e  1919  equsex  1998  nfeqf2  2001  exdistrf  2035  sb5rfOLD  2131  mo2v  2269  mo2vOLD  2270  mo2vOLDOLD  2271  moanim  2339  euan  2340  euanOLD  2341  moexex  2358  moexexOLD  2359  2eu6  2380  ceqsex  3114  sbhypf  3125  vtoclgf  3134  vtoclg1f  3135  vtoclef  3151  rspn0  3760  reusv2lem1  4604  copsexg  4687  copsexgOLD  4688  copsex2g  4690  ralxpf  5097  dmcoss  5210  fv3  5815  tz6.12c  5821  opabiota  5866  0neqopab  6243  zfregcl  7923  scottex  8206  scott0  8207  dfac5lem5  8411  zfcndpow  8897  zfcndreg  8898  zfcndinf  8899  reclem2pr  9331  uzindOLD  10850  mreiincl  14656  exisym1  28434  eu2ndop1stv  30194  bnj607  32261  bnj900  32274  bj-equsexv  32600  exlimii  32691  bj-exlimmpi  32764  bj-exlimmpbi  32765  bj-exlimmpbir  32766  dihglblem5  35301
  Copyright terms: Public domain W3C validator