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

Metamath Proof Explorer

Theorem ex-ss

Description: Example for df-ss . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion ex-ss ⊢ 1 2 ⊆ 1 2 3

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ 1 2 ⊆ 1 2 ∪ 3
2 df-tp ⊢ 1 2 3 = 1 2 ∪ 3
3 1 2 sseqtrri ⊢ 1 2 ⊆ 1 2 3