Theorem spimefv

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

Hypotheses
spimefv.1
\( \vdash \Finv x \, \varphi \)
spimefv.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \)
Proof
spimefv.1
l1
a1i _
\( \vdash \top \rightarrow \Finv x \, \varphi \)
spimefv.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
spimedv l1 _
mptru _