# Metamath Proof Explorer

## Theorem sbequ1

Description: An equality theorem for substitution. (Contributed by NM, 16-May-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020)

Ref Expression
Assertion sbequ1 ${⊢}{x}={t}\to \left({\phi }\to \left[{t}/{x}\right]{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 equeucl ${⊢}{x}={t}\to \left({y}={t}\to {x}={y}\right)$
2 ax12v ${⊢}{x}={y}\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)$
3 1 2 syl6 ${⊢}{x}={t}\to \left({y}={t}\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\right)$
4 3 com23 ${⊢}{x}={t}\to \left({\phi }\to \left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\right)$
5 4 alrimdv ${⊢}{x}={t}\to \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\right)$
6 df-sb ${⊢}\left[{t}/{x}\right]{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)$
7 5 6 syl6ibr ${⊢}{x}={t}\to \left({\phi }\to \left[{t}/{x}\right]{\phi }\right)$