Theorem iunid

Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005)

	Ref	Expression
Assertion	iunid	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-sn	⊢ { 𝑥 } = { 𝑦 ∣ 𝑦 = 𝑥 }
2		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
3	2	abbii	⊢ { 𝑦 ∣ 𝑦 = 𝑥 } = { 𝑦 ∣ 𝑥 = 𝑦 }
4	1 3	eqtri	⊢ { 𝑥 } = { 𝑦 ∣ 𝑥 = 𝑦 }
5	4	a1i	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } = { 𝑦 ∣ 𝑥 = 𝑦 } )
6	5	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝑥 = 𝑦 }
7		iunab	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝑥 = 𝑦 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝑦 }
8		risset	⊢ ( 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝑦 )
9	8	abbii	⊢ { 𝑦 ∣ 𝑦 ∈ 𝐴 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝑦 }
10		abid2	⊢ { 𝑦 ∣ 𝑦 ∈ 𝐴 } = 𝐴
11	7 9 10	3eqtr2i	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝑥 = 𝑦 } = 𝐴
12	6 11	eqtri	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴