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

Definition df-eu 2258
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 2275, eu2 2279, eu3 2280, and eu5 2292 (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 2337). (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 2254 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1650 . . . . 5  wff  x  =  y
61, 5wb 177 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1546 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1547 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 177 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff set class
This definition is referenced by:  euf  2260  eubid  2261  nfeu1  2264  nfeud2  2266  sb8eu  2272  exists1  2343  reu6  3083  euabsn2  3835  euotd  4417  iotauni  5389  iota1  5391  iotanul  5392  iotaex  5394  iota4  5395  fv3  5703  eufnfv  5931  seqomlem2  6667  aceq1  7954  dfac5  7965  iotain  27485  iotaexeu  27486  iotasbc  27487  iotavalsb  27501  sbiota1  27502  bnj89  28792
  Copyright terms: Public domain W3C validator