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	⊢ ∪ { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 }

Proof

Step	Hyp	Ref	Expression
1		prex	⊢ { 1 , 3 } ∈ V
2		prex	⊢ { 1 , 8 } ∈ V
3	1 2	unipr	⊢ ∪ { { 1 , 3 } , { 1 , 8 } } = ( { 1 , 3 } ∪ { 1 , 8 } )
4		ex-un	⊢ ( { 1 , 3 } ∪ { 1 , 8 } ) = { 1 , 3 , 8 }
5	3 4	eqtri	⊢ ∪ { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 }