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	|- PrPairs = ( v e. _V |-> { p | E. a e. v E. b e. v ( a =/= b /\ p = { a , b } ) } )

Detailed syntax breakdown

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