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 φ