Step |
Hyp |
Ref |
Expression |
1 |
|
prprval |
⊢ ( 𝑉 ∈ 𝑊 → ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } ) |
2 |
|
prssi |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → { 𝑎 , 𝑏 } ⊆ 𝑉 ) |
3 |
|
eleq1 |
⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ) ) |
4 |
3
|
adantl |
⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ) ) |
5 |
|
prex |
⊢ { 𝑎 , 𝑏 } ∈ V |
6 |
5
|
elpw |
⊢ ( { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ⊆ 𝑉 ) |
7 |
4 6
|
bitrdi |
⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ⊆ 𝑉 ) ) |
8 |
2 7
|
syl5ibrcom |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → 𝑝 ∈ 𝒫 𝑉 ) ) |
9 |
8
|
rexlimivv |
⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → 𝑝 ∈ 𝒫 𝑉 ) |
10 |
9
|
pm4.71ri |
⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ) |
11 |
10
|
a1i |
⊢ ( 𝑉 ∈ 𝑊 → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ) ) |
12 |
11
|
abbidv |
⊢ ( 𝑉 ∈ 𝑊 → { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } = { 𝑝 ∣ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) } ) |
13 |
|
df-rab |
⊢ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } = { 𝑝 ∣ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) } |
14 |
12 13
|
eqtr4di |
⊢ ( 𝑉 ∈ 𝑊 → { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } ) |
15 |
1 14
|
eqtrd |
⊢ ( 𝑉 ∈ 𝑊 → ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } ) |