Theorem eumo 2313

Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)

Assertion

Ref	Expression
eumo

Proof of Theorem eumo

Step	Hyp	Ref	Expression
1		eu5 2310	. 2
2	1	simprbi 464	1

Syntax hints:  ->wi 4  E.wex 1612  E!weu 2282  E*wmo 2283

This theorem is referenced by:  eumoi  2314  euimmo  2343  moaneu  2354  eupick  2358  2eumo  2367  2exeu  2371  2eu2  2378  2eu5  2382  moeq3  3276  euabex  4713  nfunsn  5902  dff3  6044  fnoprabg  6403  zfrep6  6768  nqerf  9329  f1otrspeq  16472  uptx  20126  txcn  20127  pm14.12  31328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-eu 2286  df-mo 2287