Theorem euex 2110

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.

Step	Hyp	Ref	Expression
1		ax-17 1575	. . 3 |- ( ph -> A. y ph )
2	1	eu1 2105	. 2 |- ( E! x ph <-> E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) )
3		exsimpl 1666	. 2 |- ( E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) -> E. x ph )
4	2, 3	sylbi 121	1 |- ( E! x ph -> E. x ph )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1396   E.wex 1541   [wsb 1811   E!weu 2080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-eu 2083

This theorem is referenced by:  eu2  2125  eu3h  2126  eu5  2128  exmoeudc  2144  eupickbi  2163  2eu2ex  2170  euxfrdc  3003  repizf  4226  eusvnf  4574  eusvnfb  4575  tz6.12c  5700  ndmfvg  5701  elfvm  5703  nfvres  5706  0fv  5708  eusvobj2  6036  fnoprabg  6154  0g0  13589  txcn  15140