Theorem speiv

Description: Inference from existential specialization. (Contributed by NM, 19-Aug-1993) (Revised by Wolf Lammen, 22-Oct-2023)

	Ref	Expression
Hypotheses	speiv.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) )
	speiv.2	⊢ 𝜓
Assertion	speiv	⊢ ∃ 𝑥 𝜑

Proof

Step	Hyp	Ref	Expression
1		speiv.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) )
2		speiv.2	⊢ 𝜓
3	2	hbth	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
4	3 1	spimew	⊢ ( 𝜓 → ∃ 𝑥 𝜑 )
5	2 4	ax-mp	⊢ ∃ 𝑥 𝜑