# Metamath Proof Explorer

## Theorem ex-pss

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

Ref Expression
Assertion ex-pss ${⊢}\left\{1,2\right\}\subset \left\{1,2,3\right\}$

### Proof

Step Hyp Ref Expression
1 ex-ss ${⊢}\left\{1,2\right\}\subseteq \left\{1,2,3\right\}$
2 3ex ${⊢}3\in \mathrm{V}$
3 2 tpid3 ${⊢}3\in \left\{1,2,3\right\}$
4 1re ${⊢}1\in ℝ$
5 1lt3 ${⊢}1<3$
6 4 5 gtneii ${⊢}3\ne 1$
7 2re ${⊢}2\in ℝ$
8 2lt3 ${⊢}2<3$
9 7 8 gtneii ${⊢}3\ne 2$
10 6 9 nelpri ${⊢}¬3\in \left\{1,2\right\}$
11 nelne1 ${⊢}\left(3\in \left\{1,2,3\right\}\wedge ¬3\in \left\{1,2\right\}\right)\to \left\{1,2,3\right\}\ne \left\{1,2\right\}$
12 3 10 11 mp2an ${⊢}\left\{1,2,3\right\}\ne \left\{1,2\right\}$
13 12 necomi ${⊢}\left\{1,2\right\}\ne \left\{1,2,3\right\}$
14 df-pss ${⊢}\left\{1,2\right\}\subset \left\{1,2,3\right\}↔\left(\left\{1,2\right\}\subseteq \left\{1,2,3\right\}\wedge \left\{1,2\right\}\ne \left\{1,2,3\right\}\right)$
15 1 13 14 mpbir2an ${⊢}\left\{1,2\right\}\subset \left\{1,2,3\right\}$