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

Definition df-eu 2150
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 2167, eu2 2171, eu3 2172, and eu5 2184 (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 2229). (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 group:    ph( x)

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  set  x
31, 2weu 2146 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1626 . . . . 5  wff  x  =  y
61, 5wb 178 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1529 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1530 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 178 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff set class
This definition is referenced by:  euf  2152  eubid  2153  nfeu1  2156  nfeud2  2158  sb8eu  2164  exists1  2235  reu6  2957  euabsn2  3701  euotd  4268  fv3  5503  tz6.12-2  5509  eufnfv  5715  iotauni  6266  iota1  6268  iotanul  6269  iotaex  6271  iota4  6272  seqomlem2  6460  aceq1  7741  dfac5  7752  iotain  27018  iotaexeu  27019  iotasbc  27020  iotavalsb  27034  sbiota1  27035  bnj89  28016
  Copyright terms: Public domain W3C validator