Theorem euex 1394

Description: Existential uniqueness implies existence.

Assertion

Ref	Expression
euex	|- (E!xph -> E.xph)

Proof of Theorem euex

Step	Hyp	Ref	Expression
1		ax-17 971	. . . 4 |- (ph -> A.yph)
2	1	eu1 1392	. . 3 |- (E!xph <-> E.x(ph /\ A.y([y / x]ph -> x = y)))
3		19.40 1094	. . 3 |- (E.x(ph /\ A.y([y / x]ph -> x = y)) -> (E.xph /\ E.xA.y([y / x]ph -> x = y)))
4	2, 3	sylbi 199	. 2 |- (E!xph -> (E.xph /\ E.xA.y([y / x]ph -> x = y)))
5	4	pm3.26d 321	1 |- (E!xph -> E.xph)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 954  E.wex 980  E!weu 1380

This theorem is referenced by:  eu2 1396  exmoeu 1413  euor2 1437  2eu2ex 1443  euxfr 1927  reurex 1928  zfrep6 3614  fnopabg 3615  tz6.12c 3740  ndmfv 3745  dff2 3817  fnoprabg 4012  aceq5lem5 4739  hlimeu 9111

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382

Copyright terms: Public domain