Metamath Proof Explorer

Theorem bj-hbyfrbi

Description: Version of bj-hbxfrbi with existential quantifiers. (Contributed by BJ, 23-Aug-2023)

Ref Expression
Assertion bj-hbyfrbi ⊢ φ ↔ ψ ∧ ∀ x φ ↔ ψ → ∃ x φ → φ ↔ ∃ x ψ → ψ

Proof

Step Hyp Ref Expression
1 exbi ⊢ ∀ x φ ↔ ψ → ∃ x φ ↔ ∃ x ψ
2 1 adantl ⊢ φ ↔ ψ ∧ ∀ x φ ↔ ψ → ∃ x φ ↔ ∃ x ψ
3 simpl ⊢ φ ↔ ψ ∧ ∀ x φ ↔ ψ → φ ↔ ψ
4 2 3 imbi12d ⊢ φ ↔ ψ ∧ ∀ x φ ↔ ψ → ∃ x φ → φ ↔ ∃ x ψ → ψ