Metamath Proof Explorer

Theorem ex-uni

Description: Example for df-uni . Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion ex-uni 
|- U. { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 }

Proof

Step Hyp Ref Expression
1 prex 
 |-  { 1 , 3 } e. _V
2 prex 
 |-  { 1 , 8 } e. _V
3 1 2 unipr 
 |-  U. { { 1 , 3 } , { 1 , 8 } } = ( { 1 , 3 } u. { 1 , 8 } )
4 ex-un 
 |-  ( { 1 , 3 } u. { 1 , 8 } ) = { 1 , 3 , 8 }
5 3 4 eqtri 
 |-  U. { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 }