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