Metamath Proof Explorer

Theorem bj-spimtv

Description: Version of spimt with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 14-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-spimtv ⊢ Ⅎ x ψ ∧ ∀ x x = y → φ → ψ → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 ax6ev ⊢ ∃ 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 19.9t ⊢ Ⅎ x ψ → ∃ x ψ ↔ ψ
7 6 biimpd ⊢ Ⅎ x ψ → ∃ x ψ → ψ
8 5 7 sylan9r ⊢ Ⅎ x ψ ∧ ∀ x x = y → φ → ψ → ∀ x φ → ψ