Definition df-spr 41728

Description: Define the function which maps a set v to the set of pairs consisting of elements of the set v. (Contributed by AV, 21-Nov-2021.)

Assertion

Ref	Expression
df-spr	|- Pairs = ( v e. _V |-> { p | E. a e. v E. b e. v p = { a , b } } )

Distinct variable group:   a, b, p, v

Detailed syntax breakdown of Definition df-spr

Step	Hyp	Ref	Expression
1		cspr 41727	. 2 class Pairs
2		vv	. . 3 setvar v
3		cvv 3200	. . 3 class _V
4		vp	. . . . . . . 8 setvar p
5	4	cv 1482	. . . . . . 7 class p
6		va	. . . . . . . . 9 setvar a
7	6	cv 1482	. . . . . . . 8 class a
8		vb	. . . . . . . . 9 setvar b
9	8	cv 1482	. . . . . . . 8 class b
10	7, 9	cpr 4179	. . . . . . 7 class { a , b }
11	5, 10	wceq 1483	. . . . . 6 wff p = { a , b }
12	2	cv 1482	. . . . . 6 class v
13	11, 8, 12	wrex 2913	. . . . 5 wff E. b e. v p = { a , b }
14	13, 6, 12	wrex 2913	. . . 4 wff E. a e. v E. b e. v p = { a , b }
15	14, 4	cab 2608	. . 3 class { p | E. a e. v E. b e. v p = { a , b } }
16	2, 3, 15	cmpt 4729	. 2 class ( v e. _V |-> { p | E. a e. v E. b e. v p = { a , b } } )
17	1, 16	wceq 1483	1 wff Pairs = ( v e. _V |-> { p | E. a e. v E. b e. v p = { a , b } } )

This definition is referenced by:  sprval  41729