Metamath Proof Explorer

Theorem snsstp1

Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013)

Ref Expression
Assertion snsstp1 
|- { A } C_ { A , B , C }

Proof

Step Hyp Ref Expression
1 snsspr1 
 |-  { A } C_ { A , B }
2 ssun1 
 |-  { A , B } C_ ( { A , B } u. { C } )
3 1 2 sstri 
 |-  { A } C_ ( { A , B } u. { C } )
4 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
5 3 4 sseqtrri 
 |-  { A } C_ { A , B , C }