# Metamath Proof Explorer

## Theorem sbco2

Description: 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.)

Ref Expression
Hypothesis sbco2.1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion sbco2 ${⊢}\left[{y}/{z}\right]\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }$

### Proof

Step Hyp Ref Expression
1 sbco2.1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
2 sbequ12 ${⊢}{z}={y}\to \left(\left[{z}/{x}\right]{\phi }↔\left[{y}/{z}\right]\left[{z}/{x}\right]{\phi }\right)$
3 sbequ ${⊢}{z}={y}\to \left(\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }\right)$
4 2 3 bitr3d ${⊢}{z}={y}\to \left(\left[{y}/{z}\right]\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }\right)$
5 4 sps ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left(\left[{y}/{z}\right]\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }\right)$
6 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
7 1 nfsb4 ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
8 3 a1i ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({z}={y}\to \left(\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }\right)\right)$
9 6 7 8 sbied ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left(\left[{y}/{z}\right]\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }\right)$
10 5 9 pm2.61i ${⊢}\left[{y}/{z}\right]\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }$