Metamath Proof Explorer


Theorem reuprg

Description: Convert a restricted existential uniqueness over a pair to a disjunction and an implication . (Contributed by AV, 2-Apr-2023)

Ref Expression
Hypotheses reuprg.1 x = A φ ψ
reuprg.2 x = B φ χ
Assertion reuprg A V B W ∃! x A B φ ψ χ χ ψ A = B

Proof

Step Hyp Ref Expression
1 reuprg.1 x = A φ ψ
2 reuprg.2 x = B φ χ
3 1 2 reuprg0 A V B W ∃! x A B φ ψ χ A = B χ ψ A = B
4 orddi ψ χ A = B χ ψ A = B ψ χ ψ ψ A = B χ A = B χ χ A = B ψ A = B
5 curryax ψ ψ A = B
6 5 biantru ψ χ ψ χ ψ ψ A = B
7 6 bicomi ψ χ ψ ψ A = B ψ χ
8 curryax χ χ A = B
9 orcom χ A = B χ χ χ A = B
10 8 9 mpbir χ A = B χ
11 10 biantrur χ A = B ψ A = B χ A = B χ χ A = B ψ A = B
12 11 bicomi χ A = B χ χ A = B ψ A = B χ A = B ψ A = B
13 pm4.79 χ A = B ψ A = B χ ψ A = B
14 12 13 bitri χ A = B χ χ A = B ψ A = B χ ψ A = B
15 7 14 anbi12i ψ χ ψ ψ A = B χ A = B χ χ A = B ψ A = B ψ χ χ ψ A = B
16 4 15 bitri ψ χ A = B χ ψ A = B ψ χ χ ψ A = B
17 3 16 bitrdi A V B W ∃! x A B φ ψ χ χ ψ A = B