Theorem eu5 2310

Description: Uniqueness in terms of "at most one." Revised to reduce dependencies on axioms. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.)

Assertion

Ref	Expression
eu5

Proof of Theorem eu5

Step	Hyp	Ref	Expression
1		abai 795	. 2
2		euex 2308	. . 3
3	2	pm4.71ri 633	. 2
4		df-mo 2287	. . 3
5	4	anbi2i 694	. 2
6	1, 3, 5	3bitr4i 277	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  E.wex 1612  E!weu 2282  E*wmo 2283

This theorem is referenced by:  exmoeu2  2311  eu3v  2312  eumo  2313  eu2  2326  eu4  2338  euim  2344  2euex  2366  2euswap  2370  2exeu  2371  2eu1OLD  2377  2eu4  2380  reu5  3073  reuss2  3777  n0moeu  3798  reusv2lem1  4653  funcnv3  5654  fnres  5702  fnopabg  5709  brprcneu  5864  dff3  6044  finnisoeu  8515  dfac2  8532  recmulnq  9363  uptx  20126  hausflf2  20499  adjeu  26808  mptfnf  27499  fzisoeu  31500  ellimciota  31620  bnj151  33935  bnj600  33977  bj-eu3f  34413

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