Step |
Hyp |
Ref |
Expression |
1 |
|
prprspr2 |
⊢ ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 } |
2 |
1
|
rabeq2i |
⊢ ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ↔ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ) |
3 |
2
|
a1i |
⊢ ( 𝑉 ∈ 𝑊 → ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ↔ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ) ) |
4 |
3
|
anbi1d |
⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ( ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ∧ 𝜑 ) ) ) |
5 |
|
anass |
⊢ ( ( ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ∧ 𝜑 ) ↔ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) |
6 |
4 5
|
bitrdi |
⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) ) |
7 |
6
|
eubidv |
⊢ ( 𝑉 ∈ 𝑊 → ( ∃! 𝑝 ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ∃! 𝑝 ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) ) |
8 |
|
df-reu |
⊢ ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) 𝜑 ↔ ∃! 𝑝 ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ) |
9 |
|
df-reu |
⊢ ( ∃! 𝑝 ∈ ( Pairs ‘ 𝑉 ) ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ↔ ∃! 𝑝 ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) |
10 |
7 8 9
|
3bitr4g |
⊢ ( 𝑉 ∈ 𝑊 → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) 𝜑 ↔ ∃! 𝑝 ∈ ( Pairs ‘ 𝑉 ) ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) |