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