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

Definition df-eu 2272
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 2313, eu2 2312, eu3v 2298, and eu5 2296 (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  setvar  x
31, 2weu 2268 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1720 . . . . 5  wff  x  =  y
61, 5wb 184 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1381 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1599 . 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  2274  mo2v  2275  mo2vOLD  2276  mo2vOLDOLD  2277  euf  2278  nfeu1  2280  nfeud2  2282  eubid  2288  euex  2294  sb8eu  2304  sb8euOLD  2305  exists1  2374  reu6  3274  euabsn2  4086  euotd  4738  iotauni  5553  iota1  5555  iotanul  5556  iotaex  5558  iota4  5559  fv3  5869  eufnfv  6131  seqomlem2  7118  aceq1  8501  dfac5  8512  wl-sb8eut  29998  iotain  31278  iotaexeu  31279  iotasbc  31280  iotavalsb  31294  sbiota1  31295  bnj89  33642
  Copyright terms: Public domain W3C validator