Definition df-spr 44882

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

Step	Hyp	Ref	Expression
1		cspr 44881	. 2 class Pairs
2		vv	. . 3 setvar 𝑣
3		cvv 3430	. . 3 class V
4		vp	. . . . . . . 8 setvar 𝑝
5	4	cv 1540	. . . . . . 7 class 𝑝
6		va	. . . . . . . . 9 setvar 𝑎
7	6	cv 1540	. . . . . . . 8 class 𝑎
8		vb	. . . . . . . . 9 setvar 𝑏
9	8	cv 1540	. . . . . . . 8 class 𝑏
10	7, 9	cpr 4568	. . . . . . 7 class {𝑎, 𝑏}
11	5, 10	wceq 1541	. . . . . 6 wff 𝑝 = {𝑎, 𝑏}
12	2	cv 1540	. . . . . 6 class 𝑣
13	11, 8, 12	wrex 3066	. . . . 5 wff ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}
14	13, 6, 12	wrex 3066	. . . 4 wff ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}
15	14, 4	cab 2716	. . 3 class {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}}
16	2, 3, 15	cmpt 5161	. 2 class (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}})
17	1, 16	wceq 1541	1 wff Pairs = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}})

This definition is referenced by:  sprval  44883