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

Theorem exlimi 1781
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed 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 1777 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1543 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537   F/wnf 1539
This theorem is referenced by:  exlimih  1782  19.41  1799  equs5a  1911  sb5rf  1984  equvin  1999  exlimiv  2023  euan  2170  moexex  2182  ceqsex  2760  sbhypf  2771  vtoclgf  2780  vtoclef  2794  copsexg  4145  copsex2g  4147  reusv2lem1  4426  ralxpf  4737  dmcoss  4851  fv3  5393  tz6.12c  5400  opabiota  6177  zfregcl  7192  scottex  7439  scott0  7440  dfac5lem5  7638  zfcndpow  8118  zfcndreg  8119  zfcndinf  8120  reclem2pr  8552  uzindOLD  9985  mreiincl  13370  exisym1  24037  stoweidlem59  26942  bnj607  27734  bnj900  27747  dihglblem5  30392
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator