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