Metamath Proof Explorer

Theorem snsspr1

Description: A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004)

Ref Expression
Assertion snsspr1 
|- { A } C_ { A , B }

Proof

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