This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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