Metamath Proof Explorer

Theorem 19.35

Description: Theorem 19.35 of Margaris p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 27-Jun-2014)

Ref Expression
Assertion 19.35 ⊢ ∃ x φ → ψ ↔ ∀ x φ → ∃ x ψ

Proof

Step Hyp Ref Expression
1 pm2.27 ⊢ φ → φ → ψ → ψ
2 1 aleximi ⊢ ∀ x φ → ∃ x φ → ψ → ∃ x ψ
3 2 com12 ⊢ ∃ x φ → ψ → ∀ x φ → ∃ x ψ
4 exnal ⊢ ∃ x ¬ φ ↔ ¬ ∀ x φ
5 pm2.21 ⊢ ¬ φ → φ → ψ
6 5 eximi ⊢ ∃ x ¬ φ → ∃ x φ → ψ
7 4 6 sylbir ⊢ ¬ ∀ x φ → ∃ x φ → ψ
8 exa1 ⊢ ∃ x ψ → ∃ x φ → ψ
9 7 8 ja ⊢ ∀ x φ → ∃ x ψ → ∃ x φ → ψ
10 3 9 impbii ⊢ ∃ x φ → ψ ↔ ∀ x φ → ∃ x ψ