Definition df-aiota 43334

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 43342); otherwise, it is not a set (see aiotaexb 43338), or even more concrete, it is the universe V (see aiotavb 43339). Since this is an alternative for df-iota 6314, 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 43338). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 43322). Only the right to left implication would hold, see (negated) iotanul 6333. For defined cases, however, both definitions df-iota 6314 and df-aiota 43334 are equivalent, see reuaiotaiota 43337. (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 43332	. 2 class (℩'𝑥𝜑)
4	1, 2	cab 2799	. . . . 5 class {𝑥 ∣ 𝜑}
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1536	. . . . . 6 class 𝑦
7	6	csn 4567	. . . . 5 class {𝑦}
8	4, 7	wceq 1537	. . . 4 wff {𝑥 ∣ 𝜑} = {𝑦}
9	8, 5	cab 2799	. . 3 class {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
10	9	cint 4876	. 2 class ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
11	3, 10	wceq 1537	1 wff (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}

This definition is referenced by:  dfaiota2  43335  reuabaiotaiota  43336  aiotaexb  43338  aiotavb  43339