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	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) ) → ( ∀ 𝑥 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑦
2		exim	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ( 𝜑 → 𝜓 ) ) )
3	1 2	mpi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) → ∃ 𝑥 ( 𝜑 → 𝜓 ) )
4		19.35	⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
5	3 4	sylib	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
6		19.9t	⊢ ( Ⅎ 𝑥 𝜓 → ( ∃ 𝑥 𝜓 ↔ 𝜓 ) )
7	6	biimpd	⊢ ( Ⅎ 𝑥 𝜓 → ( ∃ 𝑥 𝜓 → 𝜓 ) )
8	5 7	sylan9r	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) ) → ( ∀ 𝑥 𝜑 → 𝜓 ) )