Definition df-aiota

Description: Alternate version of Russell's definition of a description binder, which can be read as "the unique x such that ph ", where ph ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that ph is true (see aiotaval ); otherwise, it is not a set (see aiotaexb ), or even more concrete, it is the universe _V (see aiotavb ). Since this is an alternative for df-iota , we call this symbol iota' 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 ). With the original definition, there is no corresponding theorem ( E! x ph <-> ( iota x ph ) =/= (/) ) , because (/) can be a valid unique set satisfying a wff (see, for example, iota0def ). Only the right to left implication would hold, see (negated) iotanul . For defined cases, however, both definitions df-iota and df-aiota are equivalent, see reuaiotaiota . (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		wph	⊢ 𝜑
2	1 0	caiota	⊢ ( ℩' 𝑥 𝜑 )
3		vy	⊢ 𝑦
4	1 0	cab	⊢ { 𝑥 ∣ 𝜑 }
5	3	cv	⊢ 𝑦
6	5	csn	⊢ { 𝑦 }
7	4 6	wceq	⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 }
8	7 3	cab	⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
9	8	cint	⊢ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
10	2 9	wceq	⊢ ( ℩' 𝑥 𝜑 ) = ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }