Metamath Proof Explorer


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 V p | a v b v a b p = a b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprpr class PrPairs
1 vv setvar v
2 cvv class V
3 vp setvar p
4 va setvar a
5 1 cv setvar v
6 vb setvar b
7 4 cv setvar a
8 6 cv setvar b
9 7 8 wne wff a b
10 3 cv setvar p
11 7 8 cpr class a b
12 10 11 wceq wff p = a b
13 9 12 wa wff a b p = a b
14 13 6 5 wrex wff b v a b p = a b
15 14 4 5 wrex wff a v b v a b p = a b
16 15 3 cab class p | a v b v a b p = a b
17 1 2 16 cmpt class v V p | a v b v a b p = a b
18 0 17 wceq wff PrPairs = v V p | a v b v a b p = a b