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 ∪ ( 𝐴 ∖ { ∅ } ) = ∪ 𝐴

Proof

Step Hyp Ref Expression
1 uniun ⊢ ∪ ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } ) = ( ∪ ( 𝐴 ∖ { ∅ } ) ∪ ∪ { ∅ } )
2 undif1 ⊢ ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } ) = ( 𝐴 ∪ { ∅ } )
3 uncom ⊢ ( 𝐴 ∪ { ∅ } ) = ( { ∅ } ∪ 𝐴 )
4 2 3 eqtr2i ⊢ ( { ∅ } ∪ 𝐴 ) = ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } )
5 4 unieqi ⊢ ∪ ( { ∅ } ∪ 𝐴 ) = ∪ ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } )
6 0ex ⊢ ∅ ∈ V
7 6 unisn ⊢ ∪ { ∅ } = ∅
8 7 uneq2i ⊢ ( ∪ ( 𝐴 ∖ { ∅ } ) ∪ ∪ { ∅ } ) = ( ∪ ( 𝐴 ∖ { ∅ } ) ∪ ∅ )
9 un0 ⊢ ( ∪ ( 𝐴 ∖ { ∅ } ) ∪ ∅ ) = ∪ ( 𝐴 ∖ { ∅ } )
10 8 9 eqtr2i ⊢ ∪ ( 𝐴 ∖ { ∅ } ) = ( ∪ ( 𝐴 ∖ { ∅ } ) ∪ ∪ { ∅ } )
11 1 5 10 3eqtr4ri ⊢ ∪ ( 𝐴 ∖ { ∅ } ) = ∪ ( { ∅ } ∪ 𝐴 )
12 uniun ⊢ ∪ ( { ∅ } ∪ 𝐴 ) = ( ∪ { ∅ } ∪ ∪ 𝐴 )
13 7 uneq1i ⊢ ( ∪ { ∅ } ∪ ∪ 𝐴 ) = ( ∅ ∪ ∪ 𝐴 )
14 11 12 13 3eqtri ⊢ ∪ ( 𝐴 ∖ { ∅ } ) = ( ∅ ∪ ∪ 𝐴 )
15 uncom ⊢ ( ∅ ∪ ∪ 𝐴 ) = ( ∪ 𝐴 ∪ ∅ )
16 un0 ⊢ ( ∪ 𝐴 ∪ ∅ ) = ∪ 𝐴
17 14 15 16 3eqtri ⊢ ∪ ( 𝐴 ∖ { ∅ } ) = ∪ 𝐴