Theorem eumo 1410

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 1408	. 2 |- (E!xph <-> (E.xph /\ E*xph))
2	1	pm3.27bi 326	1 |- (E!xph -> E*xph)

Syntax hints:   -> wi 3  E.wex 979  E!weu 1379  E*wmo 1380

This theorem is referenced by:  eumoi 1411  euimmo 1419  moaneu 1429  eupick 1433  euor2 1436  2eumo 1441  2eu2 1449  2eu5 1452  moeq3 1918  euabex 2763  reuxfr 2900  dffun7 3536  zfrep6 3610  fnopabg 3611  dff2 3812  fnoprabg 4007

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382

Copyright terms: Public domain