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

Definition df-eu 2280
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 2316, eu2 2315, eu3v 2304, and eu5 2302 (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 2362). (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 2276 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1784 . . . . 5  wff  x  =  y
61, 5wb 187 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1435 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1657 . 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  2282  mo2v  2283  euf  2284  nfeu1  2286  nfeud2  2288  eubid  2294  euex  2300  sb8eu  2309  exists1  2367  reu6  3202  euabsn2  4014  euotd  4664  iotauni  5520  iota1  5522  iotanul  5523  iotaex  5525  iota4  5526  fv3  5838  eufnfv  6098  seqomlem2  7123  aceq1  8499  dfac5  8510  bnj89  29479  wl-eudf  31808  wl-euequ1f  31810  wl-sb8eut  31813  iotain  36681  iotaexeu  36682  iotasbc  36683  iotavalsb  36697  sbiota1  36698
  Copyright terms: Public domain W3C validator