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

Theorem exlimi 1917
Description: Inference associated with 19.23 1915. See exlimiv 1727 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 1915 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1626 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1617   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  exlimih  1918  equs5a  1983  equs5e  1984  equsex  2042  nfeqf2  2045  exdistrf  2079  mo2v  2291  mo2vOLD  2292  mo2vOLDOLD  2293  moanim  2347  euan  2348  moexex  2360  2eu6  2380  ceqsex  3142  sbhypf  3153  vtoclgf  3162  vtoclg1f  3163  vtoclef  3179  rspn0  3796  reusv2lem1  4638  copsexg  4722  copsex2g  4724  ralxpf  5138  dmcoss  5251  fv3  5861  tz6.12c  5867  opabiota  5911  0neqopab  6314  zfregcl  8012  scottex  8294  scott0  8295  dfac5lem5  8499  zfcndpow  8983  zfcndreg  8984  zfcndinf  8985  reclem2pr  9415  uzindOLD  10953  mreiincl  15085  brabgaf  27676  cnvoprab  27777  exisym1  30117  eu2ndop1stv  32446  bnj607  34375  bnj900  34388  bj-equsexv  34713  exlimii  34805  bj-exlimmpi  34878  bj-exlimmpbi  34879  bj-exlimmpbir  34880  dihglblem5  37422
  Copyright terms: Public domain W3C validator