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

Theorem exlimi 1972
Description: Inference associated with 19.23 1970. See exlimiv 1770 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 1970 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1666 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1657   F/wnf 1661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-nf 1662
This theorem is referenced by:  exlimih  1973  equs5a  2037  equs5e  2038  equsex  2095  nfeqf2  2100  exdistrf  2134  mo2v  2276  moanim  2328  euan  2329  moexex  2340  2eu6  2357  ceqsex  3117  sbhypf  3128  vtoclgf  3137  vtoclg1f  3138  vtoclef  3154  rspn0  3774  reusv2lem1  4625  copsexg  4706  copsex2g  4708  ralxpf  5000  dmcoss  5113  fv3  5894  tz6.12c  5900  opabiota  5944  0neqopab  6349  zfregcl  8118  scottex  8364  scott0  8365  dfac5lem5  8565  zfcndpow  9048  zfcndreg  9049  zfcndinf  9050  reclem2pr  9480  mreiincl  15501  brabgaf  28218  cnvoprab  28314  bnj607  29735  bnj900  29748  exisym1  31089  exlimii  31403  bj-exlimmpi  31481  bj-exlimmpbi  31482  bj-exlimmpbir  31483  dihglblem5  34835  eu2ndop1stv  38494
  Copyright terms: Public domain W3C validator