# Metamath Proof Explorer

## Theorem ex-dif

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

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

### Proof

Step Hyp Ref Expression
1 df-pr ${⊢}\left\{1,3\right\}=\left\{1\right\}\cup \left\{3\right\}$
2 1 difeq1i ${⊢}\left\{1,3\right\}\setminus \left\{1,8\right\}=\left(\left\{1\right\}\cup \left\{3\right\}\right)\setminus \left\{1,8\right\}$
3 difundir ${⊢}\left(\left\{1\right\}\cup \left\{3\right\}\right)\setminus \left\{1,8\right\}=\left(\left\{1\right\}\setminus \left\{1,8\right\}\right)\cup \left(\left\{3\right\}\setminus \left\{1,8\right\}\right)$
4 snsspr1 ${⊢}\left\{1\right\}\subseteq \left\{1,8\right\}$
5 ssdif0 ${⊢}\left\{1\right\}\subseteq \left\{1,8\right\}↔\left\{1\right\}\setminus \left\{1,8\right\}=\varnothing$
6 4 5 mpbi ${⊢}\left\{1\right\}\setminus \left\{1,8\right\}=\varnothing$
7 incom ${⊢}\left\{3\right\}\cap \left\{1,8\right\}=\left\{1,8\right\}\cap \left\{3\right\}$
8 1re ${⊢}1\in ℝ$
9 1lt3 ${⊢}1<3$
10 8 9 gtneii ${⊢}3\ne 1$
11 3re ${⊢}3\in ℝ$
12 3lt8 ${⊢}3<8$
13 11 12 ltneii ${⊢}3\ne 8$
14 10 13 nelpri ${⊢}¬3\in \left\{1,8\right\}$
15 disjsn ${⊢}\left\{1,8\right\}\cap \left\{3\right\}=\varnothing ↔¬3\in \left\{1,8\right\}$
16 14 15 mpbir ${⊢}\left\{1,8\right\}\cap \left\{3\right\}=\varnothing$
17 7 16 eqtri ${⊢}\left\{3\right\}\cap \left\{1,8\right\}=\varnothing$
18 disj3 ${⊢}\left\{3\right\}\cap \left\{1,8\right\}=\varnothing ↔\left\{3\right\}=\left\{3\right\}\setminus \left\{1,8\right\}$
19 17 18 mpbi ${⊢}\left\{3\right\}=\left\{3\right\}\setminus \left\{1,8\right\}$
20 19 eqcomi ${⊢}\left\{3\right\}\setminus \left\{1,8\right\}=\left\{3\right\}$
21 6 20 uneq12i ${⊢}\left(\left\{1\right\}\setminus \left\{1,8\right\}\right)\cup \left(\left\{3\right\}\setminus \left\{1,8\right\}\right)=\varnothing \cup \left\{3\right\}$
22 uncom ${⊢}\varnothing \cup \left\{3\right\}=\left\{3\right\}\cup \varnothing$
23 un0 ${⊢}\left\{3\right\}\cup \varnothing =\left\{3\right\}$
24 21 22 23 3eqtri ${⊢}\left(\left\{1\right\}\setminus \left\{1,8\right\}\right)\cup \left(\left\{3\right\}\setminus \left\{1,8\right\}\right)=\left\{3\right\}$
25 2 3 24 3eqtri ${⊢}\left\{1,3\right\}\setminus \left\{1,8\right\}=\left\{3\right\}$