Theorem euex 2112

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 2107	. 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 2082

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 2085

This theorem is referenced by:  eu2  2127  eu3h  2128  eu5  2130  exmoeudc  2146  eupickbi  2165  2eu2ex  2172  euxfrdc  3006  repizf  4231  eusvnf  4579  eusvnfb  4580  tz6.12c  5705  ndmfvg  5706  elfvm  5708  nfvres  5711  0fv  5713  eusvobj2  6044  fnoprabg  6162  0g0  13639  txcn  15266