This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊆ A B C

Proof

Step Hyp Ref Expression
1 ssun2 ⊢ C ⊆ A B ∪ C
2 df-tp ⊢ A B C = A B ∪ C
3 1 2 sseqtrri ⊢ C ⊆ A B C