Definition df-eu 2070

Description: Define existential uniqueness, i.e. "there exists exactly one x such that ph." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2081, eu2 2085, eu3 2086, and eu5 2099 (which in some cases we show with a hypothesis ph -> A.yph in place of a distinct variable condition on y and ph). Double uniqueness is tricky: E!xE!yph does not mean "exactly one x and one y " (see 2eu4 2144).

Assertion

Ref	Expression
df-eu	|- (E!xph <-> E.yA.x(ph <-> x = y))

Distinct variable groups:   x,y   ph,y

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3	1, 2	weu 2066	. 2 wff E!xph
4	2	cv 1614	. . . . . 6 class x
5		vy	. . . . . . 7 set y
6	5	cv 1614	. . . . . 6 class y
7	4, 6	wceq 1615	. . . . 5 wff x = y
8	1, 7	wb 231	. . . 4 wff (ph <-> x = y)
9	8, 2	wal 1613	. . 3 wff A.x(ph <-> x = y)
10	9, 5	wex 1644	. 2 wff E.yA.x(ph <-> x = y)
11	3, 10	wb 231	1 wff (E!xph <-> E.yA.x(ph <-> x = y))

This definition is referenced by:  euf 2072  eubid 2073  hbeu1 2076  hbeu 2077  hbeud 2078  sb8eu 2079  exists1 2150  reu6 2720  euabsn 3317  fv3 4818  eufnfv 4896  iotaequ 5271  iotanul 5272  iotaex 5273  iota4 5274  aceq1 6248  aceq5 6259  bnj77 13382  bnj89 13387  invtrgrp 16018  iotain 17466  iotaexeu 17467  iotasbc 17468  euunianOLD 17481  iotavalsb 17483  sbiota1 17484

Copyright terms: Public domain