Definition df-prpr 47500

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

Assertion

Ref	Expression
df-prpr	⊢ Pairsproper = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})

Distinct variable group:   𝑎,𝑏,𝑝,𝑣

Detailed syntax breakdown of Definition df-prpr

Step	Hyp	Ref	Expression
1		cprpr 47499	. 2 class Pairsproper
2		vv	. . 3 setvar 𝑣
3		cvv 3480	. . 3 class V
4		va	. . . . . . . . 9 setvar 𝑎
5	4	cv 1539	. . . . . . . 8 class 𝑎
6		vb	. . . . . . . . 9 setvar 𝑏
7	6	cv 1539	. . . . . . . 8 class 𝑏
8	5, 7	wne 2940	. . . . . . 7 wff 𝑎 ≠ 𝑏
9		vp	. . . . . . . . 9 setvar 𝑝
10	9	cv 1539	. . . . . . . 8 class 𝑝
11	5, 7	cpr 4628	. . . . . . . 8 class {𝑎, 𝑏}
12	10, 11	wceq 1540	. . . . . . 7 wff 𝑝 = {𝑎, 𝑏}
13	8, 12	wa 395	. . . . . 6 wff (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})
14	2	cv 1539	. . . . . 6 class 𝑣
15	13, 6, 14	wrex 3070	. . . . 5 wff ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})
16	15, 4, 14	wrex 3070	. . . 4 wff ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})
17	16, 9	cab 2714	. . 3 class {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}
18	2, 3, 17	cmpt 5225	. 2 class (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})
19	1, 18	wceq 1540	1 wff Pairsproper = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})

This definition is referenced by:  prprval  47501