This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 19.19

Description: Theorem 19.19 of Margaris p. 90. (Contributed by NM, 12-Mar-1993)

Ref Expression
Hypothesis 19.19.1 ⊢ Ⅎ x φ
Assertion 19.19 ⊢ ∀ x φ ↔ ψ → φ ↔ ∃ x ψ

Proof

Step Hyp Ref Expression
1 19.19.1 ⊢ Ⅎ x φ
2 1 19.9 ⊢ ∃ x φ ↔ φ
3 exbi ⊢ ∀ x φ ↔ ψ → ∃ x φ ↔ ∃ x ψ
4 2 3 bitr3id ⊢ ∀ x φ ↔ ψ → φ ↔ ∃ x ψ