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

Definition df-eu 2309
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 2342, eu2 2340, eu3 2331, and eu5 2339 (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 2409). (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 2305 . 2
4 vy . . . . . 6
52, 4weq 1663 . . . . 5
61, 5wb 178 . . . 4
76, 2wal 1556 . . 3
87, 4wex 1557 . 2
93, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  euf  2311  eufOLD  2312  nfeu1  2313  nfeud2  2315  eubid  2321  nfeud2OLD  2324  euex  2327  sb8eu  2333  sb8euOLD  2334  exists1  2415  reu6  3174  euabsn2  3960  euotd  4596  iotauni  5392  iota1  5394  iotanul  5395  iotaex  5397  iota4  5398  fv3  5697  eufnfv  5929  seqomlem2  6820  aceq1  8112  dfac5  8123  iotain  28520  iotaexeu  28521  iotasbc  28522  iotavalsb  28536  sbiota1  28537  bnj89  30279
  Copyright terms: Public domain W3C validator