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	⊢ Pairsproper = ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprpr	⊢ Pairsproper
1		vv	⊢ 𝑣
2		cvv	⊢ V
3		vp	⊢ 𝑝
4		va	⊢ 𝑎
5	1	cv	⊢ 𝑣
6		vb	⊢ 𝑏
7	4	cv	⊢ 𝑎
8	6	cv	⊢ 𝑏
9	7 8	wne	⊢ 𝑎 ≠ 𝑏
10	3	cv	⊢ 𝑝
11	7 8	cpr	⊢ { 𝑎 , 𝑏 }
12	10 11	wceq	⊢ 𝑝 = { 𝑎 , 𝑏 }
13	9 12	wa	⊢ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } )
14	13 6 5	wrex	⊢ ∃ 𝑏 ∈ 𝑣 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } )
15	14 4 5	wrex	⊢ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } )
16	15 3	cab	⊢ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) }
17	1 2 16	cmpt	⊢ ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } )
18	0 17	wceq	⊢ Pairsproper = ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } )