Theorem euex 2109

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 2104	. 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 1810   E!weu 2079

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 1811  df-eu 2082

This theorem is referenced by:  eu2  2124  eu3h  2125  eu5  2127  exmoeudc  2143  eupickbi  2162  2eu2ex  2169  euxfrdc  2993  repizf  4210  eusvnf  4556  eusvnfb  4557  tz6.12c  5678  ndmfvg  5679  elfvm  5681  nfvres  5684  0fv  5686  eusvobj2  6014  fnoprabg  6132  0g0  13539  txcn  15086