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 }