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

Definition df-eu 2262
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 2279, eu2 2283, eu3 2284, and eu5 2296 (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 2341). (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 2258 . 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  2264  eubid  2265  nfeu1  2268  nfeud2  2270  sb8eu  2276  exists1  2347  reu6  3087  euabsn2  3839  euotd  4421  iotauni  5393  iota1  5395  iotanul  5396  iotaex  5398  iota4  5399  fv3  5707  eufnfv  5935  seqomlem2  6671  aceq1  7958  dfac5  7969  iotain  27489  iotaexeu  27490  iotasbc  27491  iotavalsb  27505  sbiota1  27506  bnj89  28796
  Copyright terms: Public domain W3C validator