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	⊢ { 1 , 2 } ⊊ { 1 , 2 , 3 }

Proof

Step	Hyp	Ref	Expression
1		ex-ss	⊢ { 1 , 2 } ⊆ { 1 , 2 , 3 }
2		3ex	⊢ 3 ∈ V
3	2	tpid3	⊢ 3 ∈ { 1 , 2 , 3 }
4		1re	⊢ 1 ∈ ℝ
5		1lt3	⊢ 1 < 3
6	4 5	gtneii	⊢ 3 ≠ 1
7		2re	⊢ 2 ∈ ℝ
8		2lt3	⊢ 2 < 3
9	7 8	gtneii	⊢ 3 ≠ 2
10	6 9	nelpri	⊢ ¬ 3 ∈ { 1 , 2 }
11		nelne1	⊢ ( ( 3 ∈ { 1 , 2 , 3 } ∧ ¬ 3 ∈ { 1 , 2 } ) → { 1 , 2 , 3 } ≠ { 1 , 2 } )
12	3 10 11	mp2an	⊢ { 1 , 2 , 3 } ≠ { 1 , 2 }
13	12	necomi	⊢ { 1 , 2 } ≠ { 1 , 2 , 3 }
14		df-pss	⊢ ( { 1 , 2 } ⊊ { 1 , 2 , 3 } ↔ ( { 1 , 2 } ⊆ { 1 , 2 , 3 } ∧ { 1 , 2 } ≠ { 1 , 2 , 3 } ) )
15	1 13 14	mpbir2an	⊢ { 1 , 2 } ⊊ { 1 , 2 , 3 }