Theorem sb6f

Equivalence for substitution when \( y \) is not free in \( \varphi \). The implication "to the left" is sb2 and does not require the nonfreeness hypothesis. Theorem sb6 replaces the nonfreeness hypothesis with a disjoint variable condition on x , y and requires fewer axioms. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)

Hypothesis
sb6f.1
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash [ y / x ] \, \varphi \leftrightarrow \forall x \, (x = y \rightarrow \varphi) \)
Proof
sb6f.1
nf5ri _
l2
sbimi _
\( \vdash [ y / x ] \, \varphi \rightarrow [ y / x ] \, \forall y \, \varphi \)
sb4a
\( \vdash [ y / x ] \, \forall y \, \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
l4
syl l2 _
sb2
impbii l4 _