Metamath Proof Explorer

Theorem 19.23v

Description: Version of 19.23 with a disjoint variable condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

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

Proof

Step Hyp Ref Expression
1 exim ⊢ ∀ x φ → ψ → ∃ x φ → ∃ x ψ
2 ax5e ⊢ ∃ x ψ → ψ
3 1 2 syl6 ⊢ ∀ x φ → ψ → ∃ x φ → ψ
4 ax-5 ⊢ ψ → ∀ x ψ
5 4 imim2i ⊢ ∃ x φ → ψ → ∃ x φ → ∀ x ψ
6 19.38 ⊢ ∃ x φ → ∀ x ψ → ∀ x φ → ψ
7 5 6 syl ⊢ ∃ x φ → ψ → ∀ x φ → ψ
8 3 7 impbii ⊢ ∀ x φ → ψ ↔ ∃ x φ → ψ