Theorem euex 2116

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 1579	. . 3 |- ( ph -> A. y ph )
2	1	eu1 2111	. 2 |- ( E! x ph <-> E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) )
3		exsimpl 1670	. 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 1400   E.wex 1545   [wsb 1815   E!weu 2086

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-eu 2089

This theorem is referenced by:  eu2  2131  eu3h  2132  eu5  2134  exmoeudc  2150  eupickbi  2169  2eu2ex  2176  euxfrdc  3012  repizf  4242  eusvnf  4594  eusvnfb  4595  tz6.12c  5720  ndmfvg  5721  elfvm  5723  nfvres  5726  0fv  5728  eusvobj2  6061  fnoprabg  6179  0g0  13673  txcn  15299