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

Definition df-eu 1963
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 1985, eu2 2004, eu3 2006, and eu5 2007 (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 2053). (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 1960 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1447 . . . . 5  wff  x  =  y
61, 5wb 104 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1297 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1436 . 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  1965  eubidh  1966  eubid  1967  hbeu1  1970  nfeu1  1971  sb8eu  1973  nfeudv  1975  nfeuv  1978  sb8euh  1983  exists1  2056  reu6  2826  euabsn2  3539  euotd  4114  iotauni  5036  iota1  5038  iotanul  5039  euiotaex  5040  iota4  5042  fv3  5376  eufnfv  5580
  Copyright terms: Public domain W3C validator