Metamath Proof Explorer


Theorem snsspr2

Description: A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009)

Ref Expression
Assertion snsspr2 BAB

Proof

Step Hyp Ref Expression
1 ssun2 BAB
2 df-pr AB=AB
3 1 2 sseqtrri BAB