ex-dif

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

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

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

Metamath Proof Explorer