Metamath Proof Explorer


Theorem prprsprreu

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

Ref Expression
Assertion prprsprreu V W ∃! p PrPairs V φ ∃! p Pairs V p = 2 φ

Proof

Step Hyp Ref Expression
1 prprspr2 PrPairs V = p Pairs V | p = 2
2 1 rabeq2i p PrPairs V p Pairs V p = 2
3 2 a1i V W p PrPairs V p Pairs V p = 2
4 3 anbi1d V W p PrPairs V φ p Pairs V p = 2 φ
5 anass p Pairs V p = 2 φ p Pairs V p = 2 φ
6 4 5 bitrdi V W p PrPairs V φ p Pairs V p = 2 φ
7 6 eubidv V W ∃! p p PrPairs V φ ∃! p p Pairs V p = 2 φ
8 df-reu ∃! p PrPairs V φ ∃! p p PrPairs V φ
9 df-reu ∃! p Pairs V p = 2 φ ∃! p p Pairs V p = 2 φ
10 7 8 9 3bitr4g V W ∃! p PrPairs V φ ∃! p Pairs V p = 2 φ