Theorem dfiota2

Description: Alternate definition for descriptions. Definition 8.18 in Quine p. 56. (Contributed by Andrew Salmon, 30-Jun-2011)

	Ref	Expression
Assertion	dfiota2	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		df-iota	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
2		absn	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
3	2	abbii	⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }
4	3	unieqi	⊢ ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }
5	1 4	eqtri	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }