unss

Description: The union of two subclasses is a subclass. Theorem 27 of Suppes p. 27 and its converse. (Contributed by NM, 11-Jun-2004)

		Ref	Expression
	Assertion	unss	$⊢ (A \subseteq C \land B \subseteq C) \leftrightarrow A \cup B \subseteq C$

Step	Hyp	Ref	Expression
1		df-ss	$⊢ A \cup B \subseteq C \leftrightarrow \forall x (x \in (A \cup B) \to x \in C)$
2		19.26	$⊢ \forall x ((x \in A \to x \in C) \land (x \in B \to x \in C)) \leftrightarrow (\forall x (x \in A \to x \in C) \land \forall x (x \in B \to x \in C))$
3		elunant	$⊢ (x \in (A \cup B) \to x \in C) \leftrightarrow ((x \in A \to x \in C) \land (x \in B \to x \in C))$
4	3	albii	$⊢ \forall x (x \in (A \cup B) \to x \in C) \leftrightarrow \forall x ((x \in A \to x \in C) \land (x \in B \to x \in C))$
5		df-ss	$⊢ A \subseteq C \leftrightarrow \forall x (x \in A \to x \in C)$
6		df-ss	$⊢ B \subseteq C \leftrightarrow \forall x (x \in B \to x \in C)$
7	5 6	anbi12i	$⊢ (A \subseteq C \land B \subseteq C) \leftrightarrow (\forall x (x \in A \to x \in C) \land \forall x (x \in B \to x \in C))$
8	2 4 7	3bitr4i	$⊢ \forall x (x \in (A \cup B) \to x \in C) \leftrightarrow (A \subseteq C \land B \subseteq C)$
9	1 8	bitr2i	$⊢ (A \subseteq C \land B \subseteq C) \leftrightarrow A \cup B \subseteq C$

Metamath Proof Explorer