Metamath Proof Explorer


Theorem hashprlei

Description: An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion hashprlei ABFinAB2

Proof

Step Hyp Ref Expression
1 df-pr AB=AB
2 hashsnlei AFinA1
3 hashsnlei BFinB1
4 1nn0 10
5 1p1e2 1+1=2
6 1 2 3 4 4 5 hashunlei ABFinAB2