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

Step	Hyp	Ref	Expression
1		wph	. . 3
2		vx	. . 3
3	1, 2	weu 2288	. 2
4		vy	. . . . . 6
5	2, 4	weq 1655	. . . . 5
6	1, 5	wb 178	. . . 4
7	6, 2	wal 1550	. . 3
8	7, 4	wex 1551	. 2
9	3, 8	wb 178	1

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