Theorem spimvALT

Alternate proof of spimv. Note that it requires only [ax-1] through [ax-5] together with ax6e. Currently, proofs derive from ax6v, but if [ax-6] could be used instead, this proof would reduce axiom usage. (Contributed by NM, 31-Jul-1993.) Remove dependency on [ax-10]. (Revised by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
spimv.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
l0
ax6e
\( \vdash \exists x \, x = y' \)
spimv.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
eximii l0 _
19.36iv _