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

Definition df-eu 2222
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 2262, eu2 2261, eu3v 2248, and eu5 2246 (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 2311). (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 2218 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1741 . . . . 5  wff  x  =  y
61, 5wb 184 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1397 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1620 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 184 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff setvar class
This definition is referenced by:  euequ1  2224  mo2v  2225  mo2vOLD  2226  mo2vOLDOLD  2227  euf  2228  nfeu1  2230  nfeud2  2232  eubid  2238  euex  2244  sb8eu  2253  sb8euOLD  2254  exists1  2319  reu6  3213  euabsn2  4015  euotd  4662  iotauni  5472  iota1  5474  iotanul  5475  iotaex  5477  iota4  5478  fv3  5787  eufnfv  6047  seqomlem2  7034  aceq1  8411  dfac5  8422  wl-sb8eut  30187  iotain  31492  iotaexeu  31493  iotasbc  31494  iotavalsb  31508  sbiota1  31509  bnj89  34121
  Copyright terms: Public domain W3C validator