Metamath Proof Explorer


Theorem sprval

Description: The set of all unordered pairs over a given set V . (Contributed by AV, 21-Nov-2021)

Ref Expression
Assertion sprval V W Pairs V = p | a V b V p = a b

Proof

Step Hyp Ref Expression
1 df-spr Pairs = v V p | a v b v p = a b
2 1 a1i V W Pairs = v V p | a v b v p = a b
3 id v = V v = V
4 rexeq v = V b v p = a b b V p = a b
5 3 4 rexeqbidv v = V a v b v p = a b a V b V p = a b
6 5 adantl V W v = V a v b v p = a b a V b V p = a b
7 6 abbidv V W v = V p | a v b v p = a b = p | a V b V p = a b
8 elex V W V V
9 zfpair2 a b V
10 eueq a b V ∃! p p = a b
11 9 10 mpbi ∃! p p = a b
12 euabex ∃! p p = a b p | p = a b V
13 11 12 mp1i V W p | p = a b V
14 13 ralrimivw V W b V p | p = a b V
15 abrexex2g V W b V p | p = a b V p | b V p = a b V
16 14 15 mpdan V W p | b V p = a b V
17 16 ralrimivw V W a V p | b V p = a b V
18 abrexex2g V W a V p | b V p = a b V p | a V b V p = a b V
19 17 18 mpdan V W p | a V b V p = a b V
20 2 7 8 19 fvmptd V W Pairs V = p | a V b V p = a b