Theorem 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\ne \varnothing \to \bigcap A\subseteq \bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall y\in Ax\in y\right)\to \exists y\in Ax\in y$$
2	1	ex	$$⊢A\ne \varnothing \to \left(\forall y\in Ax\in y\to \exists y\in Ax\in y\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	elint2	$$⊢x\in \bigcap A\leftrightarrow \forall y\in Ax\in y$$
5		eluni2	$$⊢x\in \bigcup A\leftrightarrow \exists y\in Ax\in y$$
6	2 4 5	3imtr4g	$$⊢A\ne \varnothing \to \left(x\in \bigcap A\to x\in \bigcup A\right)$$
7	6	ssrdv	$$⊢A\ne \varnothing \to \bigcap A\subseteq \bigcup A$$