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

Metamath Proof Explorer

Theorem snsstp1

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

Ref Expression
Assertion snsstp1 ⊢ A ⊆ A B C

Proof

Step Hyp Ref Expression
1 snsspr1 ⊢ A ⊆ A B
2 ssun1 ⊢ A B ⊆ A B ∪ C
3 1 2 sstri ⊢ A ⊆ A B ∪ C
4 df-tp ⊢ A B C = A B ∪ C
5 3 4 sseqtrri ⊢ A ⊆ A B C