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	|- F/ x ph
	spimefv.2	|- ( x = y -> ( ph -> ps ) )
Assertion	spimefv	|- ( ph -> E. x ps )

Proof

Step	Hyp	Ref	Expression
1		spimefv.1	|- F/ x ph
2		spimefv.2	|- ( x = y -> ( ph -> ps ) )
3	1	a1i	|- ( T. -> F/ x ph )
4	3 2	spimedv	|- ( T. -> ( ph -> E. x ps ) )
5	4	mptru	|- ( ph -> E. x ps )