Theorem sbco2
A composition law for substitution. For versions requiring fewer
axioms, but more disjoint variable conditions, see sbco2v and
sbco2vv. Usage of this theorem is discouraged because it depends on
[ax-13]. (Contributed by NM, 30-Jun-1994.) (Revised by Mario
Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Sep-2018.)
(New usage is discouraged.)
Hypothesis
sbco2.1
\( \vdash \Finv z \, \varphi \)
Conclusion
\( \vdash [ y' / z ] \, [ z / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi \)
Proof
l0
sbequ12
\( \vdash z = y' \rightarrow ([ z / x ] \, \varphi \leftrightarrow [ y' / z ] \, [ z / x ] \, \varphi) \)
l1
sbequ
\( \vdash z = y' \rightarrow ([ z / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi) \)
l2
bitr3d l0 _
l3
sps _
\( \vdash \forall z \, z = y' \rightarrow ([ y' / z ] \, [ z / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi) \)
l4
nfa1
\( \vdash \Finv z \, \forall z \, z = y' \)
l5
nfn _
l6
sbco2.1
l7
nfsb4 _
\( \vdash \neg \forall z \, z = y' \rightarrow \Finv z \, [ y' / x ] \, \varphi \)
l8
a1i l1
l9
sbied l5 l7 _
l10
pm2.61i l3 _