Theorem dfaiota2

Description: Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in Quine p. 56. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	dfaiota2	⊢ ( ℩' 𝑥 𝜑 ) = ∩ { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		df-aiota	⊢ ( ℩' 𝑥 𝜑 ) = ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
2		absn	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
3	2	abbii	⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }
4	3	inteqi	⊢ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∩ { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }
5	1 4	eqtri	⊢ ( ℩' 𝑥 𝜑 ) = ∩ { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }