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	$$⊢\bigcup A=\bigcup _{x\in A}x$$

Proof

Step	Hyp	Ref	Expression
1		dfuni2	$$⊢\bigcup A=\left\{y|\exists x\in Ay\in x\right\}$$
2		df-iun	$$⊢\bigcup _{x\in A}x=\left\{y|\exists x\in Ay\in x\right\}$$
3	1 2	eqtr4i	$$⊢\bigcup A=\bigcup _{x\in A}x$$