Metamath Proof Explorer


Theorem hash2prb

Description: A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion hash2prb VWV=2aVbVabV=ab

Proof

Step Hyp Ref Expression
1 hash2exprb VWV=2ababV=ab
2 vex aV
3 2 prid1 aab
4 vex bV
5 4 prid2 bab
6 3 5 pm3.2i aabbab
7 eleq2 V=abaVaab
8 eleq2 V=abbVbab
9 7 8 anbi12d V=abaVbVaabbab
10 6 9 mpbiri V=abaVbV
11 10 adantl abV=abaVbV
12 11 pm4.71ri abV=abaVbVabV=ab
13 12 2exbii ababV=ababaVbVabV=ab
14 13 a1i VWababV=ababaVbVabV=ab
15 r2ex aVbVabV=ababaVbVabV=ab
16 15 bicomi abaVbVabV=abaVbVabV=ab
17 16 a1i VWabaVbVabV=abaVbVabV=ab
18 1 14 17 3bitrd VWV=2aVbVabV=ab