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

Definition df-eu 1919
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 1941, eu2 1960, eu3 1962, and eu5 1963 (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 2009). (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 1916 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1408 . . . . 5  wff  x  =  y
61, 5wb 102 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1257 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1397 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 102 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff set class
This definition is referenced by:  euf  1921  eubidh  1922  eubid  1923  hbeu1  1926  nfeu1  1927  sb8eu  1929  nfeudv  1931  nfeuv  1934  sb8euh  1939  exists1  2012  reu6  2752  euabsn2  3466  euotd  4018  iotauni  4906  iota1  4908  iotanul  4909  euiotaex  4910  iota4  4912  fv3  5224  eufnfv  5416
  Copyright terms: Public domain W3C validator