Theorem speivw

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

Hypotheses
speivw.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
speivw.2
\( \vdash \psi \)
Conclusion
\( \vdash \exists x \, \varphi \)
Proof
speivw.1
l1
biimprd _
\( \vdash x = y' \rightarrow \psi \rightarrow \varphi \)
speivw.2
\( \vdash \psi \)
speiv l1 _