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

Definition df-eu 2292
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 2309, eu2 2313, eu3 2314, and eu5 2326 (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 2371). (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 2288 . 2
4 vy . . . . . 6
52, 4weq 1655 . . . . 5
61, 5wb 178 . . . 4
76, 2wal 1550 . . 3
87, 4wex 1551 . 2
93, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  euf  2294  eubid  2295  nfeu1  2298  nfeud2  2300  sb8eu  2306  exists1  2377  reu6  3132  euabsn2  3903  euotd  4496  iotauni  5476  iota1  5478  iotanul  5479  iotaex  5481  iota4  5482  fv3  5787  eufnfv  6020  seqomlem2  6757  aceq1  8049  dfac5  8060  iotain  27773  iotaexeu  27774  iotasbc  27775  iotavalsb  27789  sbiota1  27790  bnj89  29327
  Copyright terms: Public domain W3C validator