# Metamath Proof Explorer

## Theorem sbequiOLD

Description: Obsolete proof of sbequi as of 7-Jul-2023. An equality theorem for substitution. (Contributed by NM, 14-May-1993) (Proof shortened by Wolf Lammen, 15-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbequiOLD ${⊢}{x}={y}\to \left(\left[{x}/{z}\right]{\phi }\to \left[{y}/{z}\right]{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 equtr ${⊢}{z}={x}\to \left({x}={y}\to {z}={y}\right)$
2 sbequ2 ${⊢}{z}={x}\to \left(\left[{x}/{z}\right]{\phi }\to {\phi }\right)$
3 sbequ1 ${⊢}{z}={y}\to \left({\phi }\to \left[{y}/{z}\right]{\phi }\right)$
4 2 3 syl9 ${⊢}{z}={x}\to \left({z}={y}\to \left(\left[{x}/{z}\right]{\phi }\to \left[{y}/{z}\right]{\phi }\right)\right)$
5 1 4 syld ${⊢}{z}={x}\to \left({x}={y}\to \left(\left[{x}/{z}\right]{\phi }\to \left[{y}/{z}\right]{\phi }\right)\right)$
6 ax13 ${⊢}¬{z}={x}\to \left({x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
7 sp ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to {z}={x}$
8 7 con3i ${⊢}¬{z}={x}\to ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}$
9 sb4OLD ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \left(\left[{x}/{z}\right]{\phi }\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to {\phi }\right)\right)$
10 8 9 syl ${⊢}¬{z}={x}\to \left(\left[{x}/{z}\right]{\phi }\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to {\phi }\right)\right)$
11 equeuclr ${⊢}{x}={y}\to \left({z}={y}\to {z}={x}\right)$
12 11 imim1d ${⊢}{x}={y}\to \left(\left({z}={x}\to {\phi }\right)\to \left({z}={y}\to {\phi }\right)\right)$
13 12 al2imi ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to {\phi }\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)$
14 sb2 ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \left[{y}/{z}\right]{\phi }$
15 13 14 syl6 ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to {\phi }\right)\to \left[{y}/{z}\right]{\phi }\right)$
16 10 15 syl9 ${⊢}¬{z}={x}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\left[{x}/{z}\right]{\phi }\to \left[{y}/{z}\right]{\phi }\right)\right)$
17 6 16 syld ${⊢}¬{z}={x}\to \left({x}={y}\to \left(\left[{x}/{z}\right]{\phi }\to \left[{y}/{z}\right]{\phi }\right)\right)$
18 5 17 pm2.61i ${⊢}{x}={y}\to \left(\left[{x}/{z}\right]{\phi }\to \left[{y}/{z}\right]{\phi }\right)$