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 syl6bb ⊢ A ∈ V ∧ B ∈ W → ∃! x ∈ A B φ ↔ ψ ∨ χ ∧ χ ∧ ψ → A = B