Theorem euex 1979

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 1465	. . 3 |- ( ph -> A. y ph )
2	1	eu1 1974	. 2 |- ( E! x ph <-> E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) )
3		exsimpl 1554	. 2 |- ( E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) -> E. x ph )
4	2, 3	sylbi 120	1 |- ( E! x ph -> E. x ph )

Syntax hints:   -> wi 4   /\ wa 103   A.wal 1288   E.wex 1427   [wsb 1693   E!weu 1949

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-eu 1952

This theorem is referenced by:  eu2  1993  eu3h  1994  eu5  1996  exmoeudc  2012  eupickbi  2031  2eu2ex  2038  euxfrdc  2802  repizf  3961  eusvnf  4288  eusvnfb  4289  tz6.12c  5347  ndmfvg  5348  nfvres  5350  0fv  5352  eusvobj2  5652  fnoprabg  5760