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 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 → ∃! 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 ∧ φ