Theorem sb6rfv

Reversed substitution. Version of sb6rf requiring disjoint variables, but fewer axioms. (Contributed by NM, 1-Aug-1993.) (Revised by Wolf Lammen, 7-Feb-2023.)

Hypothesis
sb6rfv.nf
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \varphi \leftrightarrow \forall y \, (y = x \rightarrow [ y / x ] \, \varphi) \)
Proof
l0
sb6rfv.nf
sbequ12r
equsalv l0 _
bicomi _