ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eu5 Structured version   Unicode version

Theorem eu5 1944
Description: Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)
Assertion
Ref Expression
eu5

Proof of Theorem eu5
StepHypRef Expression
1 euex 1927 . . 3
2 eumo 1929 . . 3
31, 2jca 290 . 2
4 df-mo 1901 . . . . 5
54biimpi 113 . . . 4
65imp 115 . . 3
76ancoms 255 . 2
83, 7impbii 117 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98  wex 1378  weu 1897  wmo 1898
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901
This theorem is referenced by:  exmoeu2  1945  euan  1953  eu4  1959  euim  1965  euexex  1982  2euex  1984  2euswapdc  1988  2exeu  1989  reu5  2516  reuss2  3211  funcnv3  4904  fnres  4958  fnopabg  4965  brprcneu  5114  dff3im  5255  recmulnqg  6375
  Copyright terms: Public domain W3C validator