Theorem eumo 1413

Description: Existential uniqueness implies "at most one."

Assertion

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

Proof of Theorem eumo

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

Syntax hints:   → wi 3  ∃wex 982  ∃!weu 1382  ∃*wmo 1383

This theorem is referenced by:  eumoi 1414  euimmo 1422  moaneu 1432  eupick 1436  euor2 1440  2eumo 1445  2eu2 1453  2eu5 1456  moeq3 1924  euabex 2773  reuxfr 2910  dffun7 3546  zfrep6 3620  fnopabg 3621  dff2 3823  fnoprabg 4018

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  df-mo 1385

Copyright terms: Public domain