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

Definition df-eu 2147
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 2164, eu2 2168, eu3 2169, and eu5 2181 (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 2226). (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 2143 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1624 . . . . 5  wff  x  =  y
61, 5wb 176 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1527 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1528 . 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  2149  eubid  2150  nfeu1  2153  nfeud2  2155  sb8eu  2161  exists1  2232  reu6  2954  euabsn2  3698  euotd  4267  iotauni  5231  iota1  5233  iotanul  5234  iotaex  5236  iota4  5237  fv3  5541  eufnfv  5752  seqomlem2  6463  aceq1  7744  dfac5  7755  iotain  27029  iotaexeu  27030  iotasbc  27031  iotavalsb  27045  sbiota1  27046  bnj89  28120
  Copyright terms: Public domain W3C validator