Theorem eumo 1388

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

Syntax hints:   -> wi 3  E.wex 956  E!weu 1357  E*wmo 1358

This theorem is referenced by:  eumoi 1389  euimmo 1397  moaneu 1407  eupick 1411  euor2 1414  2eumo 1419  2eu2 1427  2eu5 1430  moeq3 1893  euabex 2735  reuxfr 2867  dffun7 3481  zfrep6 3554  fnopabg 3555  dff2 3756  fnoprabg 3951

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360

Copyright terms: Public domain