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	$$⊢\mathrm{Pairs}=\left(v\in \mathrm{V}⟼\left\{p|\exists a\in v\exists b\in vp=\left\{a,b\right\}\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspr	$$class\mathrm{Pairs}$$
1		vv	$$setvarv$$
2		cvv	$$class\mathrm{V}$$
3		vp	$$setvarp$$
4		va	$$setvara$$
5	1	cv	$$setvarv$$
6		vb	$$setvarb$$
7	3	cv	$$setvarp$$
8	4	cv	$$setvara$$
9	6	cv	$$setvarb$$
10	8 9	cpr	$$class\left\{a,b\right\}$$
11	7 10	wceq	$$wffp=\left\{a,b\right\}$$
12	11 6 5	wrex	$$wff\exists b\in vp=\left\{a,b\right\}$$
13	12 4 5	wrex	$$wff\exists a\in v\exists b\in vp=\left\{a,b\right\}$$
14	13 3	cab	$$class\left\{p|\exists a\in v\exists b\in vp=\left\{a,b\right\}\right\}$$
15	1 2 14	cmpt	$$class\left(v\in \mathrm{V}⟼\left\{p|\exists a\in v\exists b\in vp=\left\{a,b\right\}\right\}\right)$$
16	0 15	wceq	$$wff\mathrm{Pairs}=\left(v\in \mathrm{V}⟼\left\{p|\exists a\in v\exists b\in vp=\left\{a,b\right\}\right\}\right)$$