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

Definition df-eu 2314
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 2350, eu2 2349, eu3v 2338, and eu5 2336 (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 2396). (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 2310 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1802 . . . . 5  wff  x  =  y
61, 5wb 189 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1453 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1674 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 189 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff setvar class
This definition is referenced by:  euequ1  2316  mo2v  2317  euf  2318  nfeu1  2320  nfeud2  2322  eubid  2328  euex  2334  sb8eu  2343  exists1  2401  reu6  3239  euabsn2  4056  euotd  4716  iotauni  5577  iota1  5579  iotanul  5580  iotaex  5582  iota4  5583  fv3  5901  eufnfv  6164  seqomlem2  7194  aceq1  8574  dfac5  8585  bnj89  29576  wl-eudf  31946  wl-euequ1f  31948  wl-sb8eut  31951  iotain  36812  iotaexeu  36813  iotasbc  36814  iotavalsb  36828  sbiota1  36829
  Copyright terms: Public domain W3C validator