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	$$⊢\bigcup \left\{\left\{1,3\right\},\left\{1,8\right\}\right\}=\left\{1,3,8\right\}$$

Proof

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