# Metamath Proof Explorer

## Theorem sbequ2

Description: An equality theorem for substitution. (Contributed by NM, 16-May-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020) (Proof shortened by Wolf Lammen, 3-Feb-2024)

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

### Proof

Step Hyp Ref Expression
1 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)$
2 1 biimpi ${⊢}\left[{t}/{x}\right]{\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)$
3 equvinva ${⊢}{x}={t}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {t}={y}\right)$
4 equcomi ${⊢}{t}={y}\to {y}={t}$
5 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to \left({x}={y}\to {\phi }\right)$
6 4 5 imim12i ${⊢}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\to \left({t}={y}\to \left({x}={y}\to {\phi }\right)\right)$
7 6 impcomd ${⊢}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\to \left(\left({x}={y}\wedge {t}={y}\right)\to {\phi }\right)$
8 7 aleximi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {t}={y}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 2 3 8 syl2im ${⊢}\left[{t}/{x}\right]{\phi }\to \left({x}={t}\to \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
10 ax5e ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }$
11 9 10 syl6com ${⊢}{x}={t}\to \left(\left[{t}/{x}\right]{\phi }\to {\phi }\right)$