Theorem ex-un

Description: Example for df-un . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	ex-un	⊢ ( { 1 , 3 } ∪ { 1 , 8 } ) = { 1 , 3 , 8 }

Proof

Step	Hyp	Ref	Expression
1		unass	⊢ ( ( { 1 , 3 } ∪ { 1 } ) ∪ { 8 } ) = ( { 1 , 3 } ∪ ( { 1 } ∪ { 8 } ) )
2		snsspr1	⊢ { 1 } ⊆ { 1 , 3 }
3		ssequn2	⊢ ( { 1 } ⊆ { 1 , 3 } ↔ ( { 1 , 3 } ∪ { 1 } ) = { 1 , 3 } )
4	2 3	mpbi	⊢ ( { 1 , 3 } ∪ { 1 } ) = { 1 , 3 }
5	4	uneq1i	⊢ ( ( { 1 , 3 } ∪ { 1 } ) ∪ { 8 } ) = ( { 1 , 3 } ∪ { 8 } )
6	1 5	eqtr3i	⊢ ( { 1 , 3 } ∪ ( { 1 } ∪ { 8 } ) ) = ( { 1 , 3 } ∪ { 8 } )
7		df-pr	⊢ { 1 , 8 } = ( { 1 } ∪ { 8 } )
8	7	uneq2i	⊢ ( { 1 , 3 } ∪ { 1 , 8 } ) = ( { 1 , 3 } ∪ ( { 1 } ∪ { 8 } ) )
9		df-tp	⊢ { 1 , 3 , 8 } = ( { 1 , 3 } ∪ { 8 } )
10	6 8 9	3eqtr4i	⊢ ( { 1 , 3 } ∪ { 1 , 8 } ) = { 1 , 3 , 8 }