Step |
Hyp |
Ref |
Expression |
1 |
|
prprelb |
⊢ ( 𝑉 ∈ 𝑊 → ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) ) ) |
2 |
1
|
anbi1d |
⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ( ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) ∧ 𝜑 ) ) ) |
3 |
|
anass |
⊢ ( ( ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) ∧ 𝜑 ) ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) |
4 |
2 3
|
bitrdi |
⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) ) |
5 |
4
|
eubidv |
⊢ ( 𝑉 ∈ 𝑊 → ( ∃! 𝑝 ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ∃! 𝑝 ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) ) |
6 |
|
df-reu |
⊢ ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) 𝜑 ↔ ∃! 𝑝 ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ) |
7 |
|
df-reu |
⊢ ( ∃! 𝑝 ∈ 𝒫 𝑉 ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ↔ ∃! 𝑝 ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) |
8 |
5 6 7
|
3bitr4g |
⊢ ( 𝑉 ∈ 𝑊 → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) 𝜑 ↔ ∃! 𝑝 ∈ 𝒫 𝑉 ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) |