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

Proof

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