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

Definition df-eu 2317
Description: Define existential uniqueness, i.e. "there exists exactly one such that ." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2350, eu2 2348, eu3 2339, and eu5 2347 (which in some cases we show with a hypothesis ->A. in place of a distinct variable condition on and ). Double uniqueness is tricky: does not mean "exactly one and one " (see 2eu4 2417). (Contributed by NM, 12-Aug-1993.)
Assertion
Ref Expression
df-eu
Distinct variable groups:   ,   ,
Allowed substitution hint:   ( )

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 wph . . 3
2 vx . . 3
31, 2weu 2313 . 2
4 vy . . . . . 6
52, 4weq 1671 . . . . 5
61, 5wb 178 . . . 4
76, 2wal 1564 . . 3
87, 4wex 1565 . 2
93, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  euf  2319  eufOLD  2320  nfeu1  2321  nfeud2  2323  eubid  2329  nfeud2OLD  2332  euex  2335  sb8eu  2341  sb8euOLD  2342  exists1  2423  reu6  3186  euabsn2  3975  euotd  4614  iotauni  5413  iota1  5415  iotanul  5416  iotaex  5418  iota4  5419  fv3  5720  eufnfv  5965  seqomlem2  6870  aceq1  8169  dfac5  8180  iotain  28845  iotaexeu  28846  iotasbc  28847  iotavalsb  28861  sbiota1  28862  bnj89  30556
  Copyright terms: Public domain W3C validator