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 { 𝐴 } ⊆ { 𝐴 , 𝐵 , 𝐶 }

Proof

Step Hyp Ref Expression
1 snsspr1 { 𝐴 } ⊆ { 𝐴 , 𝐵 }
2 ssun1 { 𝐴 , 𝐵 } ⊆ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
3 1 2 sstri { 𝐴 } ⊆ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
4 df-tp { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
5 3 4 sseqtrri { 𝐴 } ⊆ { 𝐴 , 𝐵 , 𝐶 }