MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eu Structured version   Unicode version

Definition df-eu 2287
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 2304, eu2 2308, eu3 2309, and eu5 2321 (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 2366). (Contributed by NM, 12-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  set  x
31, 2weu 2283 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1654 . . . . 5  wff  x  =  y
61, 5wb 178 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1550 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1551 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 178 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff set class
This definition is referenced by:  euf  2289  eubid  2290  nfeu1  2293  nfeud2  2295  sb8eu  2301  exists1  2372  reu6  3125  euabsn2  3877  euotd  4460  iotauni  5433  iota1  5435  iotanul  5436  iotaex  5438  iota4  5439  fv3  5747  eufnfv  5975  seqomlem2  6711  aceq1  8003  dfac5  8014  iotain  27608  iotaexeu  27609  iotasbc  27610  iotavalsb  27624  sbiota1  27625  bnj89  29160
  Copyright terms: Public domain W3C validator