Theorem euex 2085

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 1550	. . 3 |- ( ph -> A. y ph )
2	1	eu1 2080	. 2 |- ( E! x ph <-> E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) )
3		exsimpl 1641	. 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 1371   E.wex 1516   [wsb 1786   E!weu 2055

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-eu 2058

This theorem is referenced by:  eu2  2099  eu3h  2100  eu5  2102  exmoeudc  2118  eupickbi  2137  2eu2ex  2144  euxfrdc  2963  repizf  4167  eusvnf  4507  eusvnfb  4508  tz6.12c  5618  ndmfvg  5619  elfvm  5621  nfvres  5622  0fv  5624  eusvobj2  5942  fnoprabg  6058  0g0  13278  txcn  14817