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

Definition df-eu 2118
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 2134, eu2 2138, eu3 2139, and eu5 2151 (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 2196). (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 2114 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1620 . . . . 5  wff  x  =  y
61, 5wb 178 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1532 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1537 . 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  2120  eubid  2121  nfeu1  2124  nfeud2  2126  sb8eu  2132  exists1  2202  reu6  2893  euabsn2  3602  euotd  4160  fv3  5393  tz6.12-2  5399  eufnfv  5604  iotauni  6155  iota1  6157  iotanul  6158  iotaex  6160  iota4  6161  seqomlem2  6349  aceq1  7628  dfac5  7639  iotain  26784  iotaexeu  26785  iotasbc  26786  iotavalsb  26800  sbiota1  26801  bnj89  27533
  Copyright terms: Public domain W3C validator