Metamath Proof Explorer

Theorem snsstp3

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

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

Proof

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