Metamath Proof Explorer

Theorem unss1

Description: Subclass law for union of classes. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	unss1	$⊢ A \subseteq B \to A \cup C \subseteq B \cup C$

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2	1	orim1d	$⊢ A \subseteq B \to ((x \in A \lor x \in C) \to (x \in B \lor x \in C))$
3		elun	$⊢ x \in (A \cup C) \leftrightarrow (x \in A \lor x \in C)$
4		elun	$⊢ x \in (B \cup C) \leftrightarrow (x \in B \lor x \in C)$
5	2 3 4	3imtr4g	$⊢ A \subseteq B \to (x \in (A \cup C) \to x \in (B \cup C))$
6	5	ssrdv	$⊢ A \subseteq B \to A \cup C \subseteq B \cup C$