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

Definition df-eu 2284
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 2301, eu2 2305, eu3 2306, and eu5 2318 (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 2363). (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 2280 . 2  wff  E! x ph
4 vy . . . . . 6  set  y
52, 4weq 1653 . . . . 5  wff  x  =  y
61, 5wb 177 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1549 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1550 . 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  2286  eubid  2287  nfeu1  2290  nfeud2  2292  sb8eu  2298  exists1  2369  reu6  3115  euabsn2  3867  euotd  4449  iotauni  5422  iota1  5424  iotanul  5425  iotaex  5427  iota4  5428  fv3  5736  eufnfv  5964  seqomlem2  6700  aceq1  7990  dfac5  8001  iotain  27585  iotaexeu  27586  iotasbc  27587  iotavalsb  27601  sbiota1  27602  bnj89  29023
  Copyright terms: Public domain W3C validator