Definition df-aiota 48428

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 48438); otherwise, it is not a set (see aiotaexb 48432), or even more concrete, it is the universe V (see aiotavb 48433). Since this is an alternative for df-iota 6520, 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 48432). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 48381). Only the right to left implication would hold, see (negated) iotanul 6545. See also aiotaexim 48441 which requires sethood instead of not being empty. For defined cases, however, both definitions df-iota 6520 and df-aiota 48428 are equivalent, see reuaiotaiota 48431. (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 48426	. 2 class (℩'𝑥𝜑)
4	1, 2	cab 2741	. . . . 5 class {𝑥 ∣ 𝜑}
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1569	. . . . . 6 class 𝑦
7	6	csn 4588	. . . . 5 class {𝑦}
8	4, 7	wceq 1570	. . . 4 wff {𝑥 ∣ 𝜑} = {𝑦}
9	8, 5	cab 2741	. . 3 class {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
10	9	cint 4912	. 2 class ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
11	3, 10	wceq 1570	1 wff (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}

This definition is used by:  dfaiota2  48429  reuabaiotaiota  48430  aiotaexb  48432  aiotavb  48433