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 BABC

Proof

Step Hyp Ref Expression
1 snsspr2 BAB
2 ssun1 ABABC
3 1 2 sstri BABC
4 df-tp ABC=ABC
5 3 4 sseqtrri BABC