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∈ABφ↔∃x∈ABφ∧χ∧ψ→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∈ABφ↔ψ∨χ∧χ∧ψ→A=B
4 1 2 rexprg ⊢A∈V∧B∈W→∃x∈ABφ↔ψ∨χ
5 4 bicomd ⊢A∈V∧B∈W→ψ∨χ↔∃x∈ABφ
6 5 anbi1d ⊢A∈V∧B∈W→ψ∨χ∧χ∧ψ→A=B↔∃x∈ABφ∧χ∧ψ→A=B
7 3 6 bitrd ⊢A∈V∧B∈W→∃!x∈ABφ↔∃x∈ABφ∧χ∧ψ→A=B