ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-eu Unicode version

Definition df-eu 1980
Description: Define existential uniqueness, i.e. "there exists exactly one  x such that  ph." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2002, eu2 2021, eu3 2023, and eu5 2024 (which in some cases we show with a hypothesis  ph 
->  A. y ph in place of a distinct variable condition on 
y and  ph). Double uniqueness is tricky:  E! x E! y ph does not mean "exactly one  x and one  y " (see 2eu4 2070). (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-eu  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Distinct variable groups:    x, y    ph, y
Allowed substitution hint:    ph( x)

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
31, 2weu 1977 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1464 . . . . 5  wff  x  =  y
61, 5wb 104 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1314 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1453 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 104 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff set class
This definition is referenced by:  euf  1982  eubidh  1983  eubid  1984  hbeu1  1987  nfeu1  1988  sb8eu  1990  nfeudv  1992  nfeuv  1995  sb8euh  2000  exists1  2073  reu6  2846  euabsn2  3562  euotd  4146  iotauni  5070  iota1  5072  iotanul  5073  euiotaex  5074  iota4  5076  fv3  5412  eufnfv  5616
  Copyright terms: Public domain W3C validator