This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uni0c

Description: The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006)

		Ref	Expression
	Assertion	uni0c	$⊢ ⋃ A = \emptyset \leftrightarrow \forall x \in A x = \emptyset$

Step	Hyp	Ref	Expression
1		uni0b	$⊢ ⋃ A = \emptyset \leftrightarrow A \subseteq \{\emptyset\}$
2		dfss3	$⊢ A \subseteq \{\emptyset\} \leftrightarrow \forall x \in A x \in \{\emptyset\}$
3		velsn	$⊢ x \in \{\emptyset\} \leftrightarrow x = \emptyset$
4	3	ralbii	$⊢ \forall x \in A x \in \{\emptyset\} \leftrightarrow \forall x \in A x = \emptyset$
5	1 2 4	3bitri	$⊢ ⋃ A = \emptyset \leftrightarrow \forall x \in A x = \emptyset$