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\}\leftrightarrow \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	$$⊢\neg 3\in \left\{1,8\right\}$$
15		disjsn	$$⊢\left\{1,8\right\}\cap \left\{3\right\}=\varnothing \leftrightarrow \neg 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 \leftrightarrow \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\}$$