Definition df-eu 1613

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 1624, eu2 1629, eu3 1630, and eu5 1642 (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 1693).

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 1609	. 2 wff E!xph
4	2	cv 1135	. . . . . 6 class x
5		vy	. . . . . . 7 set y
6	5	cv 1135	. . . . . 6 class y
7	4, 6	wceq 1136	. . . . 5 wff x = y
8	1, 7	wb 162	. . . 4 wff (ph <-> x = y)
9	8, 2	wal 1134	. . 3 wff A.x(ph <-> x = y)
10	9, 5	wex 1164	. 2 wff E.yA.x(ph <-> x = y)
11	3, 10	wb 162	1 wff (E!xph <-> E.yA.x(ph <-> x = y))

This definition is referenced by:  euf 1615  eubid 1616  hbeu1 1619  hbeu 1620  sb8eu 1621  sb8euOLD 1622  exists1 1699  reu6 2276  euabsn 2917  fv3 4501  eufnfv 4582  iotaequ 4908  iotanul 4909  iotaex 4910  iota4 4911  aceq1 5687  aceq5 5698  bnj77 12229  bnj77OLD 12230  bnj89 12236  invtrgrp 14693  iotain 16063  iotaexeu 16064  iotasbc 16065  euunianOLD 16078  iotavalsb 16080  sbiota1 16081

Copyright terms: Public domain