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

Metamath Proof Explorer

Theorem snsspr1

Description: A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004)

Ref Expression
Assertion snsspr1 ⊢ A ⊆ A B

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ A ⊆ A ∪ B
2 df-pr ⊢ A B = A ∪ B
3 1 2 sseqtrri ⊢ A ⊆ A B