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

Metamath Proof Explorer

Theorem ssun1

Description: Subclass relationship for union of classes. Theorem 25 of Suppes p. 27. (Contributed by NM, 5-Aug-1993)

		Ref	Expression
	Assertion	ssun1	$⊢ A \subseteq A \cup B$

Step	Hyp	Ref	Expression
1		orc	$⊢ x \in A \to (x \in A \lor x \in B)$
2		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
3	1 2	sylibr	$⊢ x \in A \to x \in (A \cup B)$
4	3	ssriv	$⊢ A \subseteq A \cup B$