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

Metamath Proof Explorer

Theorem unidif0

Description: The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004)

Ref Expression
Assertion unidif0 
|- U. ( A \ { (/) } ) = U. A

Proof

Step Hyp Ref Expression
1 uniun 
 |-  U. ( ( A \ { (/) } ) u. { (/) } ) = ( U. ( A \ { (/) } ) u. U. { (/) } )
2 undif1 
 |-  ( ( A \ { (/) } ) u. { (/) } ) = ( A u. { (/) } )
3 uncom 
 |-  ( A u. { (/) } ) = ( { (/) } u. A )
4 2 3 eqtr2i 
 |-  ( { (/) } u. A ) = ( ( A \ { (/) } ) u. { (/) } )
5 4 unieqi 
 |-  U. ( { (/) } u. A ) = U. ( ( A \ { (/) } ) u. { (/) } )
6 0ex 
 |-  (/) e. _V
7 6 unisn 
 |-  U. { (/) } = (/)
8 7 uneq2i 
 |-  ( U. ( A \ { (/) } ) u. U. { (/) } ) = ( U. ( A \ { (/) } ) u. (/) )
9 un0 
 |-  ( U. ( A \ { (/) } ) u. (/) ) = U. ( A \ { (/) } )
10 8 9 eqtr2i 
 |-  U. ( A \ { (/) } ) = ( U. ( A \ { (/) } ) u. U. { (/) } )
11 1 5 10 3eqtr4ri 
 |-  U. ( A \ { (/) } ) = U. ( { (/) } u. A )
12 uniun 
 |-  U. ( { (/) } u. A ) = ( U. { (/) } u. U. A )
13 7 uneq1i 
 |-  ( U. { (/) } u. U. A ) = ( (/) u. U. A )
14 11 12 13 3eqtri 
 |-  U. ( A \ { (/) } ) = ( (/) u. U. A )
15 uncom 
 |-  ( (/) u. U. A ) = ( U. A u. (/) )
16 un0 
 |-  ( U. A u. (/) ) = U. A
17 14 15 16 3eqtri 
 |-  U. ( A \ { (/) } ) = U. A