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

Definition df-eu 2242
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 2259, eu2 2263, eu3 2264, and eu5 2276 (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 2321). (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 2238 . 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  2244  eubid  2245  nfeu1  2248  nfeud2  2250  sb8eu  2256  exists1  2327  reu6  3066  euabsn2  3818  euotd  4398  iotauni  5370  iota1  5372  iotanul  5373  iotaex  5375  iota4  5376  fv3  5684  eufnfv  5911  seqomlem2  6644  aceq1  7931  dfac5  7942  iotain  27286  iotaexeu  27287  iotasbc  27288  iotavalsb  27302  sbiota1  27303  bnj89  28424
  Copyright terms: Public domain W3C validator