Theorem sbco2v

A composition law for substitution. Version of sbco2 with disjoint variable conditions but not requiring [ax-13]. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 29-Apr-2023.)

Hypothesis
sbco2v.1
\( \vdash \Finv z \, \varphi \)
Conclusion
\( \vdash [ y' / z ] \, [ z / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi \)
Proof
sbco2v.1
l1
nfsbv _
sbequ
sbiev l1 _