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	$⊢ ⋃ (A ∖ \{\emptyset\}) = ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		undif1	$⊢ (A ∖ \{\emptyset\}) \cup \{\emptyset\} = A \cup \{\emptyset\}$
2	1	unieqi	$⊢ ⋃ ((A ∖ \{\emptyset\}) \cup \{\emptyset\}) = ⋃ (A \cup \{\emptyset\})$
3		uniun	$⊢ ⋃ (A \cup \{\emptyset\}) = ⋃ A \cup ⋃ \{\emptyset\}$
4		0ex	$⊢ \emptyset \in V$
5	4	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
6	5	uneq2i	$⊢ ⋃ A \cup ⋃ \{\emptyset\} = ⋃ A \cup \emptyset$
7	2 3 6	3eqtri	$⊢ ⋃ ((A ∖ \{\emptyset\}) \cup \{\emptyset\}) = ⋃ A \cup \emptyset$
8		uniun	$⊢ ⋃ ((A ∖ \{\emptyset\}) \cup \{\emptyset\}) = ⋃ (A ∖ \{\emptyset\}) \cup ⋃ \{\emptyset\}$
9	5	uneq2i	$⊢ ⋃ (A ∖ \{\emptyset\}) \cup ⋃ \{\emptyset\} = ⋃ (A ∖ \{\emptyset\}) \cup \emptyset$
10		un0	$⊢ ⋃ (A ∖ \{\emptyset\}) \cup \emptyset = ⋃ (A ∖ \{\emptyset\})$
11	8 9 10	3eqtri	$⊢ ⋃ ((A ∖ \{\emptyset\}) \cup \{\emptyset\}) = ⋃ (A ∖ \{\emptyset\})$
12		un0	$⊢ ⋃ A \cup \emptyset = ⋃ A$
13	7 11 12	3eqtr3i	$⊢ ⋃ (A ∖ \{\emptyset\}) = ⋃ A$