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⁡Vp=2∧φ

Proof

Step Hyp Ref Expression
1 prprspr2 ⊢PrPairs⁡V=p∈Pairs⁡V|p=2
2 1 reqabi ⊢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→∃!pp∈PrPairs⁡V∧φ↔∃!pp∈Pairs⁡V∧p=2∧φ
8 df-reu ⊢∃!p∈PrPairs⁡Vφ↔∃!pp∈PrPairs⁡V∧φ
9 df-reu ⊢∃!p∈Pairs⁡Vp=2∧φ↔∃!pp∈Pairs⁡V∧p=2∧φ
10 7 8 9 3bitr4g ⊢V∈W→∃!p∈PrPairs⁡Vφ↔∃!p∈Pairs⁡Vp=2∧φ