Theorem unidif0

Description: The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004) (Proof shortened by Eric Schmidt, 25-Apr-2026)

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

Proof

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