Definition df-aiota 47973

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 47983); otherwise, it is not a set (see aiotaexb 47977), or even more concrete, it is the universe V (see aiotavb 47978). Since this is an alternative for df-iota 6489, 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 47977). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 47926). Only the right to left implication would hold, see (negated) iotanul 6513. For defined cases, however, both definitions df-iota 6489 and df-aiota 47973 are equivalent, see reuaiotaiota 47976. (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 47971	. 2 class (℩'𝑥𝜑)
4	1, 2	cab 2738	. . . . 5 class {𝑥 ∣ 𝜑}
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1569	. . . . . 6 class 𝑦
7	6	csn 4584	. . . . 5 class {𝑦}
8	4, 7	wceq 1570	. . . 4 wff {𝑥 ∣ 𝜑} = {𝑦}
9	8, 5	cab 2738	. . 3 class {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
10	9	cint 4907	. 2 class ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
11	3, 10	wceq 1570	1 wff (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}

This definition is used by:  dfaiota2  47974  reuabaiotaiota  47975  aiotaexb  47977  aiotavb  47978