intssuni

Description: The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006)

		Ref	Expression
	Assertion	intssuni	$⊢ A \neq \emptyset \to ⋂ A \subseteq ⋃ A$

Step	Hyp	Ref	Expression
1		r19.2z	$⊢ (A \neq \emptyset \land \forall y \in A x \in y) \to \exists y \in A x \in y$
2	1	ex	$⊢ A \neq \emptyset \to (\forall y \in A x \in y \to \exists y \in A x \in y)$
3		vex	$⊢ x \in V$
4	3	elint2	$⊢ x \in ⋂ A \leftrightarrow \forall y \in A x \in y$
5		eluni2	$⊢ x \in ⋃ A \leftrightarrow \exists y \in A x \in y$
6	2 4 5	3imtr4g	$⊢ A \neq \emptyset \to (x \in ⋂ A \to x \in ⋃ A)$
7	6	ssrdv	$⊢ A \neq \emptyset \to ⋂ A \subseteq ⋃ A$

Metamath Proof Explorer