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) (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