Theorem sb6x

Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on [ax-13]. Usage of sb6 is preferred, which requires fewer axioms. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)

Hypothesis
sb6x.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \forall x \, (x = y' \rightarrow \varphi) \)
Proof
sb6x.1
l1
sbf _
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \varphi \)
l2
sb6x.1
biidd
equsal l2 _
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \varphi \)
bitr4i l1 _