Metamath Proof Explorer

Theorem spimt

Description: Closed theorem form of spim . (Contributed by NM, 15-Jan-2008) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 21-Mar-2023) Usage of this theorem is discouraged because it depends on ax-13 . (New usage is discouraged.)

Ref Expression
Assertion spimt ⊢ Ⅎ x ψ ∧ ∀ x x = y → φ → ψ → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 ax6e ⊢ ∃ x x = y
2 exim ⊢ ∀ x x = y → φ → ψ → ∃ x x = y → ∃ x φ → ψ
3 1 2 mpi ⊢ ∀ x x = y → φ → ψ → ∃ x φ → ψ
4 19.35 ⊢ ∃ x φ → ψ ↔ ∀ x φ → ∃ x ψ
5 3 4 sylib ⊢ ∀ x x = y → φ → ψ → ∀ x φ → ∃ x ψ
6 id ⊢ Ⅎ x ψ → Ⅎ x ψ
7 6 19.9d ⊢ Ⅎ x ψ → ∃ x ψ → ψ
8 5 7 sylan9r ⊢ Ⅎ x ψ ∧ ∀ x x = y → φ → ψ → ∀ x φ → ψ