Metamath Proof Explorer

Theorem 19.36v

Description: Version of 19.36 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020)

Ref Expression
Assertion 19.36v ⊢ ∃ x φ → ψ ↔ ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 19.35 ⊢ ∃ x φ → ψ ↔ ∀ x φ → ∃ x ψ
2 19.9v ⊢ ∃ x ψ ↔ ψ
3 2 imbi2i ⊢ ∀ x φ → ∃ x ψ ↔ ∀ x φ → ψ
4 1 3 bitri ⊢ ∃ x φ → ψ ↔ ∀ x φ → ψ