Theorem eumo 1644

Description: Existential uniqueness implies "at most one."

Assertion

Ref	Expression
eumo	|- (E!xph -> E*xph)

Proof of Theorem eumo

Step	Hyp	Ref	Expression
1		eu5 1642	. 2 |- (E!xph <-> (E.xph /\ E*xph))
2	1	pm3.27bi 351	1 |- (E!xph -> E*xph)

Syntax hints:   -> wi 3  E.wex 1164  E!weu 1609  E*wmo 1610

This theorem is referenced by:  eumoi 1645  euimmo 1653  moaneu 1667  eupick 1671  euor2OLD 1677  2eumo 1683  2eu2 1691  2eu5 1694  moeq3 2265  euabex 3329  reuxfrd 3657  dffun8OLD 4260  zfrep6 4356  fnopabg 4357  nfunsn 4517  dff3 4601  fnoprabg 4752  uptx 10018  isline1 14976  ufileu 15255  pm14.12 16067

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614

Copyright terms: Public domain