Metamath Proof Explorer

Theorem prprreueq

Description: There is a unique proper unordered pair over a given set V fulfilling a wff iff there is a unique subset of V of size two fulfilling this wff. (Contributed by AV, 29-Apr-2023)

Ref Expression
Assertion prprreueq ⊢ V ∈ W → ∃! p ∈ PrPairs ⁡ V φ ↔ ∃! p ∈ 𝒫 V p = 2 ∧ φ

Proof

Step Hyp Ref Expression
1 prprelb ⊢ V ∈ W → p ∈ PrPairs ⁡ V ↔ p ∈ 𝒫 V ∧ p = 2
2 1 anbi1d ⊢ V ∈ W → p ∈ PrPairs ⁡ V ∧ φ ↔ p ∈ 𝒫 V ∧ p = 2 ∧ φ
3 anass ⊢ p ∈ 𝒫 V ∧ p = 2 ∧ φ ↔ p ∈ 𝒫 V ∧ p = 2 ∧ φ
4 2 3 bitrdi ⊢ V ∈ W → p ∈ PrPairs ⁡ V ∧ φ ↔ p ∈ 𝒫 V ∧ p = 2 ∧ φ
5 4 eubidv ⊢ V ∈ W → ∃! p p ∈ PrPairs ⁡ V ∧ φ ↔ ∃! p p ∈ 𝒫 V ∧ p = 2 ∧ φ
6 df-reu ⊢ ∃! p ∈ PrPairs ⁡ V φ ↔ ∃! p p ∈ PrPairs ⁡ V ∧ φ
7 df-reu ⊢ ∃! p ∈ 𝒫 V p = 2 ∧ φ ↔ ∃! p p ∈ 𝒫 V ∧ p = 2 ∧ φ
8 5 6 7 3bitr4g ⊢ V ∈ W → ∃! p ∈ PrPairs ⁡ V φ ↔ ∃! p ∈ 𝒫 V p = 2 ∧ φ