Definition df-aiota 48263

Description: Alternate version of Russell's definition of a description binder, which can be read as "the unique 𝑥 such that 𝜑", where 𝜑 ordinarily contains 𝑥 as a free variable. Our definition is meaningful only when there is exactly one 𝑥 such that 𝜑 is true (see aiotaval 48273); otherwise, it is not a set (see aiotaexb 48267), or even more concrete, it is the universe V (see aiotavb 48268). Since this is an alternative for df-iota 6497, we call this symbol ℩' alternate iota in the following.

The advantage of this definition is the clear distinguishability of the defined and undefined cases: the alternate iota over a wff is defined iff it is a set (see aiotaexb 48267). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 48216). Only the right to left implication would hold, see (negated) iotanul 6522. See also aiotaexim 48276 which requires sethood instead of not being empty. For defined cases, however, both definitions df-iota 6497 and df-aiota 48263 are equivalent, see reuaiotaiota 48266. (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022.)

Assertion

Ref	Expression
df-aiota	⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Definition df-aiota

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	caiota 48261	. 2 class (℩'𝑥𝜑)
4	1, 2	cab 2738	. . . . 5 class {𝑥 ∣ 𝜑}
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1568	. . . . . 6 class 𝑦
7	6	csn 4584	. . . . 5 class {𝑦}
8	4, 7	wceq 1569	. . . 4 wff {𝑥 ∣ 𝜑} = {𝑦}
9	8, 5	cab 2738	. . 3 class {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
10	9	cint 4906	. 2 class ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
11	3, 10	wceq 1569	1 wff (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}

This definition is used by:  dfaiota2  48264  reuabaiotaiota  48265  aiotaexb  48267  aiotavb  48268