Metamath Proof Explorer

Theorem snsstp2

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

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

Proof

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