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

Theorem exlimi 2000
Description: Inference associated with 19.23 1998. See exlimiv 1780 for a version with a dv condition requiring fewer axioms. (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 1998 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1676 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1667   F/wnf 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-12 1937
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1668  df-nf 1672
This theorem is referenced by:  exlimih  2001  equs5a  2073  equs5e  2074  equsex  2131  nfeqf2  2136  exdistrf  2168  mo2v  2307  moanim  2359  euan  2360  moexex  2371  2eu6  2388  ceqsex  3051  sbhypf  3063  vtoclgf  3073  vtoclg1f  3074  vtoclef  3090  rspn0  3712  reusv2lem1  4577  copsexg  4660  copsex2g  4662  ralxpf  4959  dmcoss  5072  fv3  5861  tz6.12c  5867  opabiota  5912  0neqopab  6322  zfregcl  8096  scottex  8343  scott0  8344  dfac5lem5  8545  zfcndpow  9028  zfcndreg  9029  zfcndinf  9030  reclem2pr  9460  mreiincl  15513  brabgaf  28225  cnvoprab  28316  bnj607  29733  bnj900  29746  exisym1  31090  exlimii  31435  bj-exlimmpi  31514  bj-exlimmpbi  31515  bj-exlimmpbir  31516  dihglblem5  34868  eu2ndop1stv  38714
  Copyright terms: Public domain W3C validator