Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prpr Structured version   Visualization version   GIF version

Definition df-prpr 44073
 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
StepHypRef Expression
1 cprpr 44072 . 2 class Pairsproper
2 vv . . 3 setvar 𝑣
3 cvv 3441 . . 3 class V
4 va . . . . . . . . 9 setvar 𝑎
54cv 1537 . . . . . . . 8 class 𝑎
6 vb . . . . . . . . 9 setvar 𝑏
76cv 1537 . . . . . . . 8 class 𝑏
85, 7wne 2987 . . . . . . 7 wff 𝑎𝑏
9 vp . . . . . . . . 9 setvar 𝑝
109cv 1537 . . . . . . . 8 class 𝑝
115, 7cpr 4527 . . . . . . . 8 class {𝑎, 𝑏}
1210, 11wceq 1538 . . . . . . 7 wff 𝑝 = {𝑎, 𝑏}
138, 12wa 399 . . . . . 6 wff (𝑎𝑏𝑝 = {𝑎, 𝑏})
142cv 1537 . . . . . 6 class 𝑣
1513, 6, 14wrex 3107 . . . . 5 wff 𝑏𝑣 (𝑎𝑏𝑝 = {𝑎, 𝑏})
1615, 4, 14wrex 3107 . . . 4 wff 𝑎𝑣𝑏𝑣 (𝑎𝑏𝑝 = {𝑎, 𝑏})
1716, 9cab 2776 . . 3 class {𝑝 ∣ ∃𝑎𝑣𝑏𝑣 (𝑎𝑏𝑝 = {𝑎, 𝑏})}
182, 3, 17cmpt 5111 . 2 class (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎𝑣𝑏𝑣 (𝑎𝑏𝑝 = {𝑎, 𝑏})})
191, 18wceq 1538 1 wff Pairsproper = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎𝑣𝑏𝑣 (𝑎𝑏𝑝 = {𝑎, 𝑏})})
 Colors of variables: wff setvar class This definition is referenced by:  prprval  44074
 Copyright terms: Public domain W3C validator