Theorem sbid2

An identity law for substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Check out sbid2vw for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)

Hypothesis
sbid2.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow \varphi \)
Proof
l0
sbco
\( \vdash [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow [ y / x ] \, \varphi \)
sbid2.1
sbf _
\( \vdash [ y / x ] \, \varphi \leftrightarrow \varphi \)
bitri l0 _