This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }