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

Definition df-eu 1946
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 1968, eu2 1987, eu3 1989, and eu5 1990 (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 2036). (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 1943 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1433 . . . . 5  wff  x  =  y
61, 5wb 103 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1283 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1422 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 103 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff set class
This definition is referenced by:  euf  1948  eubidh  1949  eubid  1950  hbeu1  1953  nfeu1  1954  sb8eu  1956  nfeudv  1958  nfeuv  1961  sb8euh  1966  exists1  2039  reu6  2792  euabsn2  3485  euotd  4044  iotauni  4944  iota1  4946  iotanul  4947  euiotaex  4948  iota4  4950  fv3  5271  eufnfv  5463
  Copyright terms: Public domain W3C validator