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 = a b → ψ ↔ χ
reupr.x ⊢ p = x y → ψ ↔ θ
Assertion reuprpr ⊢ X ∈ V → ∃! p ∈ PrPairs ⁡ X ψ ↔ ∃ a ∈ X ∃ b ∈ X a ≠ b ∧ χ ∧ ∀ x ∈ X ∀ y ∈ X x ≠ y ∧ θ → x y = a b

Proof

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