Theorem ex-in

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

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

Proof

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