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 } u. { 3 } )
2 1 difeq1i 
 |-  ( { 1 , 3 } \ { 1 , 8 } ) = ( ( { 1 } u. { 3 } ) \ { 1 , 8 } )
3 difundir 
 |-  ( ( { 1 } u. { 3 } ) \ { 1 , 8 } ) = ( ( { 1 } \ { 1 , 8 } ) u. ( { 3 } \ { 1 , 8 } ) )
4 snsspr1 
 |-  { 1 } C_ { 1 , 8 }
5 ssdif0 
 |-  ( { 1 } C_ { 1 , 8 } <-> ( { 1 } \ { 1 , 8 } ) = (/) )
6 4 5 mpbi 
 |-  ( { 1 } \ { 1 , 8 } ) = (/)
7 incom 
 |-  ( { 3 } i^i { 1 , 8 } ) = ( { 1 , 8 } i^i { 3 } )
8 1re 
 |-  1 e. RR
9 1lt3 
 |-  1 < 3
10 8 9 gtneii 
 |-  3 =/= 1
11 3re 
 |-  3 e. RR
12 3lt8 
 |-  3 < 8
13 11 12 ltneii 
 |-  3 =/= 8
14 10 13 nelpri 
 |-  -. 3 e. { 1 , 8 }
15 disjsn 
 |-  ( ( { 1 , 8 } i^i { 3 } ) = (/) <-> -. 3 e. { 1 , 8 } )
16 14 15 mpbir 
 |-  ( { 1 , 8 } i^i { 3 } ) = (/)
17 7 16 eqtri 
 |-  ( { 3 } i^i { 1 , 8 } ) = (/)
18 disj3 
 |-  ( ( { 3 } i^i { 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 } ) u. ( { 3 } \ { 1 , 8 } ) ) = ( (/) u. { 3 } )
22 uncom 
 |-  ( (/) u. { 3 } ) = ( { 3 } u. (/) )
23 un0 
 |-  ( { 3 } u. (/) ) = { 3 }
24 21 22 23 3eqtri 
 |-  ( ( { 1 } \ { 1 , 8 } ) u. ( { 3 } \ { 1 , 8 } ) ) = { 3 }
25 2 3 24 3eqtri 
 |-  ( { 1 , 3 } \ { 1 , 8 } ) = { 3 }