Definition df-iota 5089

Description: Define Russell's definition description binder, which can be read as "the unique x such that ph," where ph ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that ph is true (see iotaval 5096); otherwise, it evaluates to the empty set (see iotanul 5098).

Assertion

Ref	Expression
df-iota	|- (iotaxph) = U.{y | {x | ph} = {y}}

Distinct variable groups:   x,y   ph,y

Detailed syntax breakdown of Definition df-iota

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3	1, 2	cio 5087	. 2 class (iotaxph)
4	1, 2	cab 1871	. . . . 5 class {x | ph}
5		vy	. . . . . . 7 set y
6	5	cv 1297	. . . . . 6 class y
7	6	csn 3044	. . . . 5 class {y}
8	4, 7	wceq 1298	. . . 4 wff {x | ph} = {y}
9	8, 5	cab 1871	. . 3 class {y | {x | ph} = {y}}
10	9	cuni 3177	. 2 class U.{y | {x | ph} = {y}}
11	3, 10	wceq 1298	1 wff (iotaxph) = U.{y | {x | ph} = {y}}

This definition is referenced by:  dfiota2 5090  hbiota1 5091  hbiota 5092  iotaeq 5093  iotabi 5094

Copyright terms: Public domain