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

Metamath Proof Explorer

Theorem intssuni2

Description: Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006)

		Ref	Expression
	Assertion	intssuni2	$⊢ (A \subseteq B \land A \neq \emptyset) \to ⋂ A \subseteq ⋃ B$

Step	Hyp	Ref	Expression
1		intssuni	$⊢ A \neq \emptyset \to ⋂ A \subseteq ⋃ A$
2		uniss	$⊢ A \subseteq B \to ⋃ A \subseteq ⋃ B$
3	1 2	sylan9ssr	$⊢ (A \subseteq B \land A \neq \emptyset) \to ⋂ A \subseteq ⋃ B$