MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eu5 Unicode version

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
StepHypRef Expression
1 abai 795 . 2
2 euex 2308 . . 3
32pm4.71ri 633 . 2
4 df-mo 2287 . . 3
54anbi2i 694 . 2
61, 3, 53bitr4i 277 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator