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	⊢ ( { 1 , 3 } ∩ { 1 , 8 } ) = { 1 }

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 1 , 8 } = ( { 1 } ∪ { 8 } )
2	1	ineq2i	⊢ ( { 1 , 3 } ∩ { 1 , 8 } ) = ( { 1 , 3 } ∩ ( { 1 } ∪ { 8 } ) )
3		indi	⊢ ( { 1 , 3 } ∩ ( { 1 } ∪ { 8 } ) ) = ( ( { 1 , 3 } ∩ { 1 } ) ∪ ( { 1 , 3 } ∩ { 8 } ) )
4		snsspr1	⊢ { 1 } ⊆ { 1 , 3 }
5		sseqin2	⊢ ( { 1 } ⊆ { 1 , 3 } ↔ ( { 1 , 3 } ∩ { 1 } ) = { 1 } )
6	4 5	mpbi	⊢ ( { 1 , 3 } ∩ { 1 } ) = { 1 }
7		1re	⊢ 1 ∈ ℝ
8		1lt8	⊢ 1 < 8
9	7 8	gtneii	⊢ 8 ≠ 1
10		3re	⊢ 3 ∈ ℝ
11		3lt8	⊢ 3 < 8
12	10 11	gtneii	⊢ 8 ≠ 3
13	9 12	nelpri	⊢ ¬ 8 ∈ { 1 , 3 }
14		disjsn	⊢ ( ( { 1 , 3 } ∩ { 8 } ) = ∅ ↔ ¬ 8 ∈ { 1 , 3 } )
15	13 14	mpbir	⊢ ( { 1 , 3 } ∩ { 8 } ) = ∅
16	6 15	uneq12i	⊢ ( ( { 1 , 3 } ∩ { 1 } ) ∪ ( { 1 , 3 } ∩ { 8 } ) ) = ( { 1 } ∪ ∅ )
17		un0	⊢ ( { 1 } ∪ ∅ ) = { 1 }
18	16 17	eqtri	⊢ ( ( { 1 , 3 } ∩ { 1 } ) ∪ ( { 1 , 3 } ∩ { 8 } ) ) = { 1 }
19	3 18	eqtri	⊢ ( { 1 , 3 } ∩ ( { 1 } ∪ { 8 } ) ) = { 1 }
20	2 19	eqtri	⊢ ( { 1 , 3 } ∩ { 1 , 8 } ) = { 1 }