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

Definition df-eu 2286
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 2327, eu2 2326, eu3v 2312, and eu5 2310 (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 2380). (Contributed by NM, 12-Aug-1993.)
Assertion
Ref Expression
df-eu
Distinct variable groups:   ,   ,

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 wph . . 3
2 vx . . 3
31, 2weu 2282 . 2
4 vy . . . . . 6
52, 4weq 1733 . . . . 5
61, 5wb 184 . . . 4
76, 2wal 1393 . . 3
87, 4wex 1612 . 2
93, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  euequ1  2288  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  euf  2292  nfeu1  2294  nfeud2  2296  eubid  2302  euex  2308  sb8eu  2318  sb8euOLD  2319  exists1  2388  reu6  3288  euabsn2  4101  euotd  4753  iotauni  5568  iota1  5570  iotanul  5571  iotaex  5573  iota4  5574  fv3  5884  eufnfv  6146  seqomlem2  7135  aceq1  8519  dfac5  8530  wl-sb8eut  30022  iotain  31324  iotaexeu  31325  iotasbc  31326  iotavalsb  31340  sbiota1  31341  bnj89  33774
  Copyright terms: Public domain W3C validator