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