Theorem euex 1392

Description: Existential uniqueness implies existence.

Assertion

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

Proof of Theorem euex

Step	Hyp	Ref	Expression
1		ax-17 969	. . . 4 |- (ph -> A.yph)
2	1	eu1 1390	. . 3 |- (E!xph <-> E.x(ph /\ A.y([y / x]ph -> x = y)))
3		19.40 1092	. . 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 952  E.wex 978  E!weu 1378

This theorem is referenced by:  eu2 1394  exmoeu 1411  euor2 1435  2eu2ex 1441  euxfr 1923  reurex 1924  zfrep6 3606  fnopabg 3607  tz6.12c 3731  ndmfv 3736  dff2 3808  fnoprabg 4003  aceq5lem5 4719  hlimeu 9050

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380

Copyright terms: Public domain