Theorem sbtrt

Partially closed form of sbtr. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by BJ, 4-Jun-2019.) (New usage is discouraged.)

Hypothesis
sbtrt.nf
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \forall y \, [ y / x ] \, \varphi \rightarrow \varphi \)
Proof
l0
stdpc4
\( \vdash \forall y \, [ y / x ] \, \varphi \rightarrow [ x / y ] \, [ y / x ] \, \varphi \)
sbtrt.nf
sbid2 _
\( \vdash [ x / y ] \, [ y / x ] \, \varphi \leftrightarrow \varphi \)
sylib l0 _