Theorem ex-ss

Description: Example for df-ss . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	ex-ss	$$⊢\left\{1,2\right\}\subseteq \left\{1,2,3\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢\left\{1,2\right\}\subseteq \left\{1,2\right\}\cup \left\{3\right\}$$
2		df-tp	$$⊢\left\{1,2,3\right\}=\left\{1,2\right\}\cup \left\{3\right\}$$
3	1 2	sseqtrri	$$⊢\left\{1,2\right\}\subseteq \left\{1,2,3\right\}$$