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

Theorem exlimi 1801
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 1797 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1536 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528   F/wnf 1531
This theorem is referenced by:  19.41  1815  equs5a  1828  sb5rf  2030  euan  2200  moexex  2212  ceqsex  2822  sbhypf  2833  vtoclgf  2842  vtoclef  2856  copsexg  4252  copsex2g  4254  reusv2lem1  4535  ralxpf  4830  dmcoss  4944  fv3  5541  tz6.12c  5547  opabiota  6293  zfregcl  7308  scottex  7555  scott0  7556  dfac5lem5  7754  zfcndpow  8238  zfcndreg  8239  zfcndinf  8240  reclem2pr  8672  uzindOLD  10106  mreiincl  13498  exisym1  24863  stoweidlem59  27808  bnj607  28948  bnj900  28961  dihglblem5  31488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator