Theorem spimfv

Specialization, using implicit substitution. Version of spim with a disjoint variable condition, which does not require [ax-13]. See spimvw for a version with two disjoint variable conditions, requiring fewer axioms, and spimv for another variant. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 31-May-2019.)

Hypotheses
spimfv.nf
\( \vdash \Finv x \, \psi \)
spimfv.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
l0
spimfv.nf
l1
ax6ev
\( \vdash \exists x \, x = y' \)
spimfv.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
eximii l1 _
19.36i l0 _