Metamath Proof Explorer

Theorem sbequ2OLD

Description: Obsolete version of sbequ2 as of 3-Feb-2024. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 25-Feb-2018) Revise df-sb . (Revised by BJ, 22-Dec-2020) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 equvinva ${⊢}{x}={t}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {t}={y}\right)$
2 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)$
3 equcomi ${⊢}{t}={y}\to {y}={t}$
4 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to \left({x}={y}\to {\phi }\right)$
5 3 4 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)$
6 5 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)$
7 6 alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={y}\wedge {t}={y}\right)\to {\phi }\right)$
8 2 7 sylbi ${⊢}\left[{t}/{x}\right]{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={y}\wedge {t}={y}\right)\to {\phi }\right)$
9 19.23v ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={y}\wedge {t}={y}\right)\to {\phi }\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {t}={y}\right)\to {\phi }\right)$
10 8 9 sylib ${⊢}\left[{t}/{x}\right]{\phi }\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {t}={y}\right)\to {\phi }\right)$
11 1 10 syl5com ${⊢}{x}={t}\to \left(\left[{t}/{x}\right]{\phi }\to {\phi }\right)$