Metamath Proof Explorer

Theorem reuprpr

Description: There is a unique proper unordered pair fulfilling a wff iff there are uniquely two different sets fulfilling a corresponding wff. (Contributed by AV, 30-Apr-2023)

Ref Expression
Hypotheses reupr.a ⊢p=ab→ψ↔χ
reupr.x ⊢p=xy→ψ↔θ
Assertion reuprpr ⊢X∈V→∃!p∈PrPairs⁡Xψ↔∃a∈X∃b∈Xa≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab

Proof

Step Hyp Ref Expression
1 reupr.a ⊢p=ab→ψ↔χ
2 reupr.x ⊢p=xy→ψ↔θ
3 prprsprreu ⊢X∈V→∃!p∈PrPairs⁡Xψ↔∃!p∈Pairs⁡Xp=2∧ψ
4 fveqeq2 ⊢p=ab→p=2↔ab=2
5 hashprg ⊢a∈V∧b∈V→a≠b↔ab=2
6 5 el2v ⊢a≠b↔ab=2
7 4 6 bitr4di ⊢p=ab→p=2↔a≠b
8 7 1 anbi12d ⊢p=ab→p=2∧ψ↔a≠b∧χ
9 fveqeq2 ⊢p=xy→p=2↔xy=2
10 hashprg ⊢x∈V∧y∈V→x≠y↔xy=2
11 10 el2v ⊢x≠y↔xy=2
12 9 11 bitr4di ⊢p=xy→p=2↔x≠y
13 12 2 anbi12d ⊢p=xy→p=2∧ψ↔x≠y∧θ
14 8 13 reupr ⊢X∈V→∃!p∈Pairs⁡Xp=2∧ψ↔∃a∈X∃b∈Xa≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab
15 df-3an ⊢a≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab↔a≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab
16 15 bicomi ⊢a≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab↔a≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab
17 16 a1i ⊢X∈V→a≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab↔a≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab
18 17 2rexbidv ⊢X∈V→∃a∈X∃b∈Xa≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab↔∃a∈X∃b∈Xa≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab
19 3 14 18 3bitrd ⊢X∈V→∃!p∈PrPairs⁡Xψ↔∃a∈X∃b∈Xa≠b∧χ∧∀x∈X∀y∈Xx≠y∧θ→xy=ab