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	⊢ { 1 , 2 } ⊆ { 1 , 2 , 3 }

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ { 1 , 2 } ⊆ ( { 1 , 2 } ∪ { 3 } )
2		df-tp	⊢ { 1 , 2 , 3 } = ( { 1 , 2 } ∪ { 3 } )
3	1 2	sseqtrri	⊢ { 1 , 2 } ⊆ { 1 , 2 , 3 }