Theorem spimefv

Description: Version of spime with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 31-May-2019)

	Ref	Expression
Hypotheses	spimefv.1	$$⊢Ⅎx\phi$$
	spimefv.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
Assertion	spimefv	$$⊢\phi \to \exists x\psi$$

Proof

Step	Hyp	Ref	Expression
1		spimefv.1	$$⊢Ⅎx\phi$$
2		spimefv.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
3	1	a1i	$$⊢\top \to Ⅎx\phi$$
4	3 2	spimedv	$$⊢\top \to \left(\phi \to \exists x\psi \right)$$
5	4	mptru	$$⊢\phi \to \exists x\psi$$