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