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

Metamath Proof Explorer

Theorem 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 }

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { 1 , 3 } = ( { 1 } ∪ { 3 } )
2 1 difeq1i ⊢ ( { 1 , 3 } ∖ { 1 , 8 } ) = ( ( { 1 } ∪ { 3 } ) ∖ { 1 , 8 } )
3 difundir ⊢ ( ( { 1 } ∪ { 3 } ) ∖ { 1 , 8 } ) = ( ( { 1 } ∖ { 1 , 8 } ) ∪ ( { 3 } ∖ { 1 , 8 } ) )
4 snsspr1 ⊢ { 1 } ⊆ { 1 , 8 }
5 ssdif0 ⊢ ( { 1 } ⊆ { 1 , 8 } ↔ ( { 1 } ∖ { 1 , 8 } ) = ∅ )
6 4 5 mpbi ⊢ ( { 1 } ∖ { 1 , 8 } ) = ∅
7 incom ⊢ ( { 3 } ∩ { 1 , 8 } ) = ( { 1 , 8 } ∩ { 3 } )
8 1re ⊢ 1 ∈ ℝ
9 1lt3 ⊢ 1 < 3
10 8 9 gtneii ⊢ 3 ≠ 1
11 3re ⊢ 3 ∈ ℝ
12 3lt8 ⊢ 3 < 8
13 11 12 ltneii ⊢ 3 ≠ 8
14 10 13 nelpri ⊢ ¬ 3 ∈ { 1 , 8 }
15 disjsn ⊢ ( ( { 1 , 8 } ∩ { 3 } ) = ∅ ↔ ¬ 3 ∈ { 1 , 8 } )
16 14 15 mpbir ⊢ ( { 1 , 8 } ∩ { 3 } ) = ∅
17 7 16 eqtri ⊢ ( { 3 } ∩ { 1 , 8 } ) = ∅
18 disj3 ⊢ ( ( { 3 } ∩ { 1 , 8 } ) = ∅ ↔ { 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 } ) ∪ ( { 3 } ∖ { 1 , 8 } ) ) = ( ∅ ∪ { 3 } )
22 uncom ⊢ ( ∅ ∪ { 3 } ) = ( { 3 } ∪ ∅ )
23 un0 ⊢ ( { 3 } ∪ ∅ ) = { 3 }
24 21 22 23 3eqtri ⊢ ( ( { 1 } ∖ { 1 , 8 } ) ∪ ( { 3 } ∖ { 1 , 8 } ) ) = { 3 }
25 2 3 24 3eqtri ⊢ ( { 1 , 3 } ∖ { 1 , 8 } ) = { 3 }