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

Definition df-eu 2270
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 2309, eu2 2308, eu3v 2296, and eu5 2294 (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 2358). (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  setvar  x
31, 2weu 2266 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1783 . . . . 5  wff  x  =  y
61, 5wb 187 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1435 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1659 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 187 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff setvar class
This definition is referenced by:  euequ1  2272  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  euf  2276  nfeu1  2278  nfeud2  2280  eubid  2286  euex  2292  sb8eu  2301  sb8euOLD  2302  exists1  2366  reu6  3266  euabsn2  4074  euotd  4722  iotauni  5577  iota1  5579  iotanul  5580  iotaex  5582  iota4  5583  fv3  5894  eufnfv  6154  seqomlem2  7176  aceq1  8546  dfac5  8557  bnj89  29315  wl-sb8eut  31610  iotain  36405  iotaexeu  36406  iotasbc  36407  iotavalsb  36421  sbiota1  36422
  Copyright terms: Public domain W3C validator