Metamath Proof Explorer

Theorem reurexprg

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

Ref Expression
Hypotheses reuprg.1 ⊢ x = A → φ ↔ ψ
reuprg.2 ⊢ x = B → φ ↔ χ
Assertion reurexprg ⊢ A ∈ V ∧ B ∈ W → ∃! x ∈ A B φ ↔ ∃ x ∈ A B φ ∧ χ ∧ ψ → A = B

Proof

Step Hyp Ref Expression
1 reuprg.1 ⊢ x = A → φ ↔ ψ
2 reuprg.2 ⊢ x = B → φ ↔ χ
3 1 2 reuprg ⊢ A ∈ V ∧ B ∈ W → ∃! x ∈ A B φ ↔ ψ ∨ χ ∧ χ ∧ ψ → A = B
4 1 2 rexprg ⊢ A ∈ V ∧ B ∈ W → ∃ x ∈ A B φ ↔ ψ ∨ χ
5 4 bicomd ⊢ A ∈ V ∧ B ∈ W → ψ ∨ χ ↔ ∃ x ∈ A B φ
6 5 anbi1d ⊢ A ∈ V ∧ B ∈ W → ψ ∨ χ ∧ χ ∧ ψ → A = B ↔ ∃ x ∈ A B φ ∧ χ ∧ ψ → A = B
7 3 6 bitrd ⊢ A ∈ V ∧ B ∈ W → ∃! x ∈ A B φ ↔ ∃ x ∈ A B φ ∧ χ ∧ ψ → A = B