Definition df-aiota 44577

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 44587); otherwise, it is not a set (see aiotaexb 44581), or even more concrete, it is the universe V (see aiotavb 44582). Since this is an alternative for df-iota 6391, 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 44581). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 44532). Only the right to left implication would hold, see (negated) iotanul 6411. For defined cases, however, both definitions df-iota 6391 and df-aiota 44577 are equivalent, see reuaiotaiota 44580. (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 44575	. 2 class (℩'𝑥𝜑)
4	1, 2	cab 2715	. . . . 5 class {𝑥 ∣ 𝜑}
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1538	. . . . . 6 class 𝑦
7	6	csn 4561	. . . . 5 class {𝑦}
8	4, 7	wceq 1539	. . . 4 wff {𝑥 ∣ 𝜑} = {𝑦}
9	8, 5	cab 2715	. . 3 class {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
10	9	cint 4879	. 2 class ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
11	3, 10	wceq 1539	1 wff (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}

This definition is referenced by:  dfaiota2  44578  reuabaiotaiota  44579  aiotaexb  44581  aiotavb  44582