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

Metamath Proof Explorer

Theorem ex-uni

Description: Example for df-uni . Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016)

		Ref	Expression
	Assertion	ex-uni	$⊢ ⋃ \{\{1, 3\}, \{1, 8\}\} = \{1, 3, 8\}$

Step	Hyp	Ref	Expression
1		prex	$⊢ \{1, 3\} \in V$
2		prex	$⊢ \{1, 8\} \in V$
3	1 2	unipr	$⊢ ⋃ \{\{1, 3\}, \{1, 8\}\} = \{1, 3\} \cup \{1, 8\}$
4		ex-un	$⊢ \{1, 3\} \cup \{1, 8\} = \{1, 3, 8\}$
5	3 4	eqtri	$⊢ ⋃ \{\{1, 3\}, \{1, 8\}\} = \{1, 3, 8\}$