Theorem eumo 1404

Description: Existential uniqueness implies "at most one."

Assertion

Ref	Expression
eumo	⊢ (∃!xφ → ∃*xφ)

Proof of Theorem eumo

Step	Hyp	Ref	Expression
1		eu5 1402	. 2 ⊢ (∃!xφ ↔ (∃xφ ⋀ ∃*xφ))
2	1	pm3.27bi 326	1 ⊢ (∃!xφ → ∃*xφ)

Syntax hints:   → wi 3  ∃wex 977  ∃!weu 1373  ∃*wmo 1374

This theorem is referenced by:  eumoi 1405  euimmo 1413  moaneu 1423  eupick 1427  euor2 1430  2eumo 1435  2eu2 1443  2eu5 1446  moeq3 1912  euabex 2757  reuxfr 2894  dffun7 3526  zfrep6 3600  fnopabg 3601  dff2 3802  fnoprabg 3997

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376

Copyright terms: Public domain