Definition df-spr

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspr	|- Pairs
1		vv	|- v
2		cvv	|- _V
3		vp	|- p
4		va	|- a
5	1	cv	|- v
6		vb	|- b
7	3	cv	|- p
8	4	cv	|- a
9	6	cv	|- b
10	8 9	cpr	|- { a , b }
11	7 10	wceq	|- p = { a , b }
12	11 6 5	wrex	|- E. b e. v p = { a , b }
13	12 4 5	wrex	|- E. a e. v E. b e. v p = { a , b }
14	13 3	cab	|- { p | E. a e. v E. b e. v p = { a , b } }
15	1 2 14	cmpt	|- ( v e. _V |-> { p | E. a e. v E. b e. v p = { a , b } } )
16	0 15	wceq	|- Pairs = ( v e. _V |-> { p | E. a e. v E. b e. v p = { a , b } } )