Theorem euex 1396

Description: Existential uniqueness implies existence.

Assertion

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

Proof of Theorem euex

Step	Hyp	Ref	Expression
1		ax-17 973	. . . 4 |- (ph -> A.yph)
2	1	eu1 1394	. . 3 |- (E!xph <-> E.x(ph /\ A.y([y / x]ph -> x = y)))
3		19.40 1096	. . 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 956  E.wex 982  E!weu 1382

This theorem is referenced by:  eu2 1398  exmoeu 1415  euor2 1440  2eu2ex 1446  euxfr 1930  reurex 1931  zfrep6 3621  fnopabg 3622  tz6.12c 3747  ndmfv 3752  dff2 3824  fnoprabg 4019  aceq5lem5 4756  hlimeu 9113

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384

Copyright terms: Public domain