NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  eu5 Unicode version

Theorem eu5 2242
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 1619 . . 3  F/
21eu3 2230 . 2
31mo2 2233 . . 3
43anbi2i 675 . 2
52, 4bitr4i 243 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176   wa 358  wal 1540  wex 1541   wceq 1642  weu 2204  wmo 2205
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209
This theorem is referenced by:  eu4  2243  eumo  2244  exmoeu2  2247  euim  2254  euan  2261  2euex  2276  2euswap  2280  2exeu  2281  2eu1  2284  reu5  2824  reuss2  3535  n0moeu  3562  funeu  5131  funcnv3  5157  fnres  5199  fnopabg  5205  dff3  5420  fnce  6176
  Copyright terms: Public domain W3C validator