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

Metamath Proof Explorer

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 }