Theorem sbco2vv

A composition law for substitution. Version of sbco2 with disjoint variable conditions and fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 29-Apr-2023.)

Conclusion
\( \vdash [ y' / z ] \, [ z / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi \)
Proof
l0
sbequ
\( \vdash z = w \rightarrow ([ z / x ] \, \varphi \leftrightarrow [ w / x ] \, \varphi) \)
sbequ
\( \vdash w = y' \rightarrow ([ w / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi) \)
sbievw2 l0 _