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