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

Theorem exlimi 1970
Description: Inference associated with 19.23 1968. See exlimiv 1769 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 1968 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1668 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1659   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664
This theorem is referenced by:  exlimih  1971  equs5a  2035  equs5e  2036  equsex  2093  nfeqf2  2097  exdistrf  2131  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  moanim  2328  euan  2329  moexex  2341  2eu6  2361  ceqsex  3123  sbhypf  3134  vtoclgf  3143  vtoclg1f  3144  vtoclef  3160  rspn0  3780  reusv2lem1  4626  copsexg  4707  copsex2g  4709  ralxpf  5001  dmcoss  5114  fv3  5894  tz6.12c  5900  opabiota  5944  0neqopab  6349  zfregcl  8109  scottex  8355  scott0  8356  dfac5lem5  8556  zfcndpow  9040  zfcndreg  9041  zfcndinf  9042  reclem2pr  9472  mreiincl  15453  brabgaf  28055  cnvoprab  28151  bnj607  29515  bnj900  29528  exisym1  30869  exlimii  31184  bj-exlimmpi  31262  bj-exlimmpbi  31263  bj-exlimmpbir  31264  dihglblem5  34575  eu2ndop1stv  38014
  Copyright terms: Public domain W3C validator