Theorem uniiun

Description: Class union in terms of indexed union. Definition in Stoll p. 43. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥

Proof

Step	Hyp	Ref	Expression
1		dfuni2	⊢ ∪ 𝐴 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 }
2		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝑥 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 }
3	1 2	eqtr4i	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥