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

Theorem eu5 2318
 Description: Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
eu5

Proof of Theorem eu5
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfv 1629 . . 3
21eu3 2306 . 2
31mo2 2309 . . 3
43anbi2i 676 . 2
52, 4bitr4i 244 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wal 1549  wex 1550  weu 2280  wmo 2281 This theorem is referenced by:  eu4  2319  eumo  2320  exmoeu2  2323  euim  2330  euan  2337  2euex  2352  2euswap  2356  2exeu  2357  2eu1  2360  reu5  2913  reuss2  3613  n0moeu  3632  reusv2lem1  4716  funcnv3  5504  fnres  5553  fnopabg  5560  brprcneu  5713  dff3  5874  finnisoeu  7986  dfac2  8003  recmulnq  8833  uptx  17649  hausflf2  18022  adjeu  23384  mptfnf  24065  bnj151  29185  bnj600  29227 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285
 Copyright terms: Public domain W3C validator