Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-spr Structured version   Visualization version   GIF version

Definition df-spr 44493
Description: Define the function which maps a set 𝑣 to the set of pairs consisting of elements of the set 𝑣. (Contributed by AV, 21-Nov-2021.)
Assertion
Ref Expression
df-spr Pairs = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎𝑣𝑏𝑣 𝑝 = {𝑎, 𝑏}})
Distinct variable group:   𝑎,𝑏,𝑝,𝑣

Detailed syntax breakdown of Definition df-spr
StepHypRef Expression
1 cspr 44492 . 2 class Pairs
2 vv . . 3 setvar 𝑣
3 cvv 3398 . . 3 class V
4 vp . . . . . . . 8 setvar 𝑝
54cv 1541 . . . . . . 7 class 𝑝
6 va . . . . . . . . 9 setvar 𝑎
76cv 1541 . . . . . . . 8 class 𝑎
8 vb . . . . . . . . 9 setvar 𝑏
98cv 1541 . . . . . . . 8 class 𝑏
107, 9cpr 4518 . . . . . . 7 class {𝑎, 𝑏}
115, 10wceq 1542 . . . . . 6 wff 𝑝 = {𝑎, 𝑏}
122cv 1541 . . . . . 6 class 𝑣
1311, 8, 12wrex 3054 . . . . 5 wff 𝑏𝑣 𝑝 = {𝑎, 𝑏}
1413, 6, 12wrex 3054 . . . 4 wff 𝑎𝑣𝑏𝑣 𝑝 = {𝑎, 𝑏}
1514, 4cab 2716 . . 3 class {𝑝 ∣ ∃𝑎𝑣𝑏𝑣 𝑝 = {𝑎, 𝑏}}
162, 3, 15cmpt 5110 . 2 class (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎𝑣𝑏𝑣 𝑝 = {𝑎, 𝑏}})
171, 16wceq 1542 1 wff Pairs = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎𝑣𝑏𝑣 𝑝 = {𝑎, 𝑏}})
Colors of variables: wff setvar class
This definition is referenced by:  sprval  44494
  Copyright terms: Public domain W3C validator