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

Step	Hyp	Ref	Expression
1		wph	. . 3
2		vx	. . 3
3	1, 2	weu 2282	. 2
4		vy	. . . . . 6
5	2, 4	weq 1733	. . . . 5
6	1, 5	wb 184	. . . 4
7	6, 2	wal 1393	. . 3
8	7, 4	wex 1612	. 2
9	3, 8	wb 184	1

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