Theorem iunid

Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005) (Proof shortened by SN, 15-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑥 } }
2		clel5	⊢ ( 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝑥 )
3		velsn	⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
4	3	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑥 } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝑥 )
5	2 4	bitr4i	⊢ ( 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑥 } )
6	5	eqabi	⊢ 𝐴 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑥 } }
7	1 6	eqtr4i	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴