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

Definition df-eu 2041
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 2063, eu2 2082, eu3 2084, and eu5 2085 (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 2131). (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 2038 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1514 . . . . 5  wff  x  =  y
61, 5wb 105 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1362 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1503 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 105 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff set class
This definition is referenced by:  euf  2043  eubidh  2044  eubid  2045  hbeu1  2048  nfeu1  2049  sb8eu  2051  nfeudv  2053  nfeuv  2056  sb8euh  2061  exists1  2134  cbvreuvw  2724  reu6  2941  euabsn2  3676  euotd  4272  iotauni  5208  iota1  5210  iotanul  5211  euiotaex  5212  iota4  5215  eliotaeu  5224  fv3  5557  eufnfv  5767
  Copyright terms: Public domain W3C validator