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

Definition df-eu 2274
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 2320, eu2 2319, eu3v 2302, and eu5 2300 (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 2385). (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  setvar  x
31, 2weu 2270 . 2  wff  E! x ph
4 vy . . . . . 6  setvar  y
52, 4weq 1700 . . . . 5  wff  x  =  y
61, 5wb 184 . . . 4  wff  ( ph  <->  x  =  y )
76, 2wal 1372 . . 3  wff  A. x
( ph  <->  x  =  y
)
87, 4wex 1591 . 2  wff  E. y A. x ( ph  <->  x  =  y )
93, 8wb 184 1  wff  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
Colors of variables: wff setvar class
This definition is referenced by:  euequ1  2276  mo2v  2277  mo2vOLD  2278  mo2vOLDOLD  2279  euf  2280  eufOLD  2281  nfeu1  2283  nfeud2  2285  eubid  2291  nfeud2OLD  2297  euex  2298  sb8eu  2309  sb8euOLD  2310  sb8euOLDOLD  2311  exists1  2393  reu6  3287  euabsn2  4093  euotd  4743  iotauni  5556  iota1  5558  iotanul  5559  iotaex  5561  iota4  5562  fv3  5872  eufnfv  6127  seqomlem2  7108  aceq1  8489  dfac5  8500  wl-sb8eut  29587  iotain  30859  iotaexeu  30860  iotasbc  30861  iotavalsb  30875  sbiota1  30876  bnj89  32731
  Copyright terms: Public domain W3C validator