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

Definition df-eu 2160
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 2177, eu2 2181, eu3 2182, and eu5 2194 (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 2239). (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 2156 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1633 . . . . 5  wff  x  =  y
61, 5wb 176 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1530 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1531 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 176 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff set class
This definition is referenced by:  euf  2162  eubid  2163  nfeu1  2166  nfeud2  2168  sb8eu  2174  exists1  2245  reu6  2967  euabsn2  3711  euotd  4283  iotauni  5247  iota1  5249  iotanul  5250  iotaex  5252  iota4  5253  fv3  5557  eufnfv  5768  seqomlem2  6479  aceq1  7760  dfac5  7771  iotain  27720  iotaexeu  27721  iotasbc  27722  iotavalsb  27736  sbiota1  27737  bnj89  29063
  Copyright terms: Public domain W3C validator