Definition df-prpr

Description: Define the function which maps a set v to the set of proper unordered pairs consisting of exactly two (different) elements of the set v . (Contributed by AV, 29-Apr-2023)

	Ref	Expression
Assertion	df-prpr	$$⊢\mathrm{PrPairs}=\left(v\in \mathrm{V}⟼\left\{p|\exists a\in v\exists b\in v\left(a\ne b\wedge p=\left\{a,b\right\}\right)\right\}\right)$$

Detailed syntax breakdown

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