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

Definition df-eu 2291
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 2308, eu2 2312, eu3 2313, and eu5 2325 (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 2370). (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 2287 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1654 . . . . 5  wff  x  =  y
61, 5wb 178 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1550 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1551 . 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  2293  eubid  2294  nfeu1  2297  nfeud2  2299  sb8eu  2305  exists1  2376  reu6  3129  euabsn2  3899  euotd  4486  iotauni  5459  iota1  5461  iotanul  5462  iotaex  5464  iota4  5465  fv3  5773  eufnfv  6001  seqomlem2  6737  aceq1  8029  dfac5  8040  iotain  27632  iotaexeu  27633  iotasbc  27634  iotavalsb  27648  sbiota1  27649  bnj89  29184
  Copyright terms: Public domain W3C validator