Metamath Proof Explorer

Theorem pairreueq

Description: Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023)

Ref Expression
Hypothesis pairreueq.p ⊢ P = x ∈ 𝒫 V | x = 2
Assertion pairreueq ⊢ ∃! p ∈ P φ ↔ ∃! p ∈ 𝒫 V p = 2 ∧ φ

Proof

Step Hyp Ref Expression
1 pairreueq.p ⊢ P = x ∈ 𝒫 V | x = 2
2 fveqeq2 ⊢ x = p → x = 2 ↔ p = 2
3 2 1 elrab2 ⊢ p ∈ P ↔ p ∈ 𝒫 V ∧ p = 2
4 3 anbi1i ⊢ p ∈ P ∧ φ ↔ p ∈ 𝒫 V ∧ p = 2 ∧ φ
5 anass ⊢ p ∈ 𝒫 V ∧ p = 2 ∧ φ ↔ p ∈ 𝒫 V ∧ p = 2 ∧ φ
6 4 5 bitri ⊢ p ∈ P ∧ φ ↔ p ∈ 𝒫 V ∧ p = 2 ∧ φ
7 6 eubii ⊢ ∃! p p ∈ P ∧ φ ↔ ∃! p p ∈ 𝒫 V ∧ p = 2 ∧ φ
8 df-reu ⊢ ∃! p ∈ P φ ↔ ∃! p p ∈ P ∧ φ
9 df-reu ⊢ ∃! p ∈ 𝒫 V p = 2 ∧ φ ↔ ∃! p p ∈ 𝒫 V ∧ p = 2 ∧ φ
10 7 8 9 3bitr4i ⊢ ∃! p ∈ P φ ↔ ∃! p ∈ 𝒫 V p = 2 ∧ φ