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 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 ↦ { 𝑝 ∣ ∃ 𝑎𝑣𝑏𝑣 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } )