ex-in

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

		Ref	Expression
	Assertion	ex-in	$⊢ \{1, 3\} \cap \{1, 8\} = \{1\}$

Step	Hyp	Ref	Expression
1		df-pr	$⊢ \{1, 8\} = \{1\} \cup \{8\}$
2	1	ineq2i	$⊢ \{1, 3\} \cap \{1, 8\} = \{1, 3\} \cap (\{1\} \cup \{8\})$
3		indi	$⊢ \{1, 3\} \cap (\{1\} \cup \{8\}) = (\{1, 3\} \cap \{1\}) \cup (\{1, 3\} \cap \{8\})$
4		snsspr1	$⊢ \{1\} \subseteq \{1, 3\}$
5		sseqin2	$⊢ \{1\} \subseteq \{1, 3\} \leftrightarrow \{1, 3\} \cap \{1\} = \{1\}$
6	4 5	mpbi	$⊢ \{1, 3\} \cap \{1\} = \{1\}$
7		1re	$⊢ 1 \in ℝ$
8		1lt8	$⊢ 1 < 8$
9	7 8	gtneii	$⊢ 8 \neq 1$
10		3re	$⊢ 3 \in ℝ$
11		3lt8	$⊢ 3 < 8$
12	10 11	gtneii	$⊢ 8 \neq 3$
13	9 12	nelpri	$⊢ \neg 8 \in \{1, 3\}$
14		disjsn	$⊢ \{1, 3\} \cap \{8\} = \emptyset \leftrightarrow \neg 8 \in \{1, 3\}$
15	13 14	mpbir	$⊢ \{1, 3\} \cap \{8\} = \emptyset$
16	6 15	uneq12i	$⊢ (\{1, 3\} \cap \{1\}) \cup (\{1, 3\} \cap \{8\}) = \{1\} \cup \emptyset$
17		un0	$⊢ \{1\} \cup \emptyset = \{1\}$
18	16 17	eqtri	$⊢ (\{1, 3\} \cap \{1\}) \cup (\{1, 3\} \cap \{8\}) = \{1\}$
19	3 18	eqtri	$⊢ \{1, 3\} \cap (\{1\} \cup \{8\}) = \{1\}$
20	2 19	eqtri	$⊢ \{1, 3\} \cap \{1, 8\} = \{1\}$

Metamath Proof Explorer