Metamath Proof Explorer


Theorem hash2prde

Description: A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017)

Ref Expression
Assertion hash2prde V W V = 2 a b a b V = a b

Proof

Step Hyp Ref Expression
1 hash2pr V W V = 2 a b V = a b
2 equid b = b
3 vex a V
4 vex b V
5 3 4 preqsn a b = b a = b b = b
6 eqeq2 a b = b V = a b V = b
7 fveq2 V = b V = b
8 hashsng b V b = 1
9 8 elv b = 1
10 7 9 eqtrdi V = b V = 1
11 eqeq1 V = 2 V = 1 2 = 1
12 1ne2 1 2
13 df-ne 1 2 ¬ 1 = 2
14 pm2.21 ¬ 1 = 2 1 = 2 a b
15 13 14 sylbi 1 2 1 = 2 a b
16 12 15 ax-mp 1 = 2 a b
17 16 eqcoms 2 = 1 a b
18 11 17 syl6bi V = 2 V = 1 a b
19 18 adantl V W V = 2 V = 1 a b
20 10 19 syl5com V = b V W V = 2 a b
21 6 20 syl6bi a b = b V = a b V W V = 2 a b
22 21 impcomd a b = b V W V = 2 V = a b a b
23 5 22 sylbir a = b b = b V W V = 2 V = a b a b
24 2 23 mpan2 a = b V W V = 2 V = a b a b
25 ax-1 a b V W V = 2 V = a b a b
26 24 25 pm2.61ine V W V = 2 V = a b a b
27 simpr V W V = 2 V = a b V = a b
28 26 27 jca V W V = 2 V = a b a b V = a b
29 28 ex V W V = 2 V = a b a b V = a b
30 29 2eximdv V W V = 2 a b V = a b a b a b V = a b
31 1 30 mpd V W V = 2 a b a b V = a b