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∈Vp=ab

Proof

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