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 }