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

Definition df-eu 2121
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 2137, eu2 2141, eu3 2142, and eu5 2154 (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 2199). (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  set  x
31, 2weu 2117 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1620 . . . . 5  wff  x  =  y
61, 5wb 178 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1532 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1537 . 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  2123  eubid  2124  nfeu1  2127  nfeud2  2129  sb8eu  2135  exists1  2205  reu6  2922  euabsn2  3658  euotd  4225  fv3  5460  tz6.12-2  5466  eufnfv  5672  iotauni  6223  iota1  6225  iotanul  6226  iotaex  6228  iota4  6229  seqomlem2  6417  aceq1  7698  dfac5  7709  iotain  26971  iotaexeu  26972  iotasbc  26973  iotavalsb  26987  sbiota1  26988  bnj89  27780
  Copyright terms: Public domain W3C validator