ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  euex Unicode version

Theorem euex 1979
Description: Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
euex  |-  ( E! x ph  ->  E. x ph )

Proof of Theorem euex
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ax-17 1465 . . 3  |-  ( ph  ->  A. y ph )
21eu1 1974 . 2  |-  ( E! x ph  <->  E. x
( ph  /\  A. y
( [ y  /  x ] ph  ->  x  =  y ) ) )
3 exsimpl 1554 . 2  |-  ( E. x ( ph  /\  A. y ( [ y  /  x ] ph  ->  x  =  y ) )  ->  E. x ph )
42, 3sylbi 120 1  |-  ( E! x ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103   A.wal 1288   E.wex 1427   [wsb 1693   E!weu 1949
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474
This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-eu 1952
This theorem is referenced by:  eu2  1993  eu3h  1994  eu5  1996  exmoeudc  2012  eupickbi  2031  2eu2ex  2038  euxfrdc  2802  repizf  3961  eusvnf  4288  eusvnfb  4289  tz6.12c  5347  ndmfvg  5348  nfvres  5350  0fv  5352  eusvobj2  5652  fnoprabg  5760
  Copyright terms: Public domain W3C validator