Metamath Proof Explorer

Theorem ssuni

Description: Subclass relationship for class union. (Contributed by NM, 24-May-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by JJ, 26-Jul-2021)

		Ref	Expression
	Assertion	ssuni	$⊢ (A \subseteq B \land B \in C) \to A \subseteq ⋃ C$

Proof

Step	Hyp	Ref	Expression
1		elunii	$⊢ (x \in B \land B \in C) \to x \in ⋃ C$
2	1	expcom	$⊢ B \in C \to (x \in B \to x \in ⋃ C)$
3	2	imim2d	$⊢ B \in C \to ((x \in A \to x \in B) \to (x \in A \to x \in ⋃ C))$
4	3	alimdv	$⊢ B \in C \to (\forall x (x \in A \to x \in B) \to \forall x (x \in A \to x \in ⋃ C))$
5		df-ss	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
6		df-ss	$⊢ A \subseteq ⋃ C \leftrightarrow \forall x (x \in A \to x \in ⋃ C)$
7	4 5 6	3imtr4g	$⊢ B \in C \to (A \subseteq B \to A \subseteq ⋃ C)$
8	7	impcom	$⊢ (A \subseteq B \land B \in C) \to A \subseteq ⋃ C$