Theorem spvv

Specialization, using implicit substitution. Version of spv with a disjoint variable condition, which does not require [ax-7], [ax-12], [ax-13]. (Contributed by NM, 30-Aug-1993.) (Revised by BJ, 31-May-2019.)

Hypothesis

spvv.1

\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)

Conclusion

\( \vdash \forall x \, \varphi \rightarrow \psi \)

Proof

spvv.1

biimpd _

\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)

spimvw _