Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  { 1 , 2 } C_ ( { 1 , 2 } u. { 3 } )
2 df-tp 
 |-  { 1 , 2 , 3 } = ( { 1 , 2 } u. { 3 } )
3 1 2 sseqtrri 
 |-  { 1 , 2 } C_ { 1 , 2 , 3 }