Theorem ex-un

Description: Example for df-un . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	ex-un	$$⊢\left\{1,3\right\}\cup \left\{1,8\right\}=\left\{1,3,8\right\}$$

Proof

Step	Hyp	Ref	Expression
1		unass	$$⊢\left(\left\{1,3\right\}\cup \left\{1\right\}\right)\cup \left\{8\right\}=\left\{1,3\right\}\cup \left(\left\{1\right\}\cup \left\{8\right\}\right)$$
2		snsspr1	$$⊢\left\{1\right\}\subseteq \left\{1,3\right\}$$
3		ssequn2	$$⊢\left\{1\right\}\subseteq \left\{1,3\right\}\leftrightarrow \left\{1,3\right\}\cup \left\{1\right\}=\left\{1,3\right\}$$
4	2 3	mpbi	$$⊢\left\{1,3\right\}\cup \left\{1\right\}=\left\{1,3\right\}$$
5	4	uneq1i	$$⊢\left(\left\{1,3\right\}\cup \left\{1\right\}\right)\cup \left\{8\right\}=\left\{1,3\right\}\cup \left\{8\right\}$$
6	1 5	eqtr3i	$$⊢\left\{1,3\right\}\cup \left(\left\{1\right\}\cup \left\{8\right\}\right)=\left\{1,3\right\}\cup \left\{8\right\}$$
7		df-pr	$$⊢\left\{1,8\right\}=\left\{1\right\}\cup \left\{8\right\}$$
8	7	uneq2i	$$⊢\left\{1,3\right\}\cup \left\{1,8\right\}=\left\{1,3\right\}\cup \left(\left\{1\right\}\cup \left\{8\right\}\right)$$
9		df-tp	$$⊢\left\{1,3,8\right\}=\left\{1,3\right\}\cup \left\{8\right\}$$
10	6 8 9	3eqtr4i	$$⊢\left\{1,3\right\}\cup \left\{1,8\right\}=\left\{1,3,8\right\}$$