# Metamath Proof Explorer

## 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\}↔\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\}$