# Metamath Proof Explorer

## Theorem bj-ssblem1

Description: A lemma for the definiens of df-sb . An instance of sp proved without it. Note: it has a common subproof with sbjust . (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ssblem1 ${⊢}\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({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 equequ1 ${⊢}{y}={z}\to \left({y}={t}↔{z}={t}\right)$
2 equequ2 ${⊢}{y}={z}\to \left({x}={y}↔{x}={z}\right)$
3 2 imbi1d ${⊢}{y}={z}\to \left(\left({x}={y}\to {\phi }\right)↔\left({x}={z}\to {\phi }\right)\right)$
4 3 albidv ${⊢}{y}={z}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={z}\to {\phi }\right)\right)$
5 1 4 imbi12d ${⊢}{y}={z}\to \left(\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)↔\left({z}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={z}\to {\phi }\right)\right)\right)$
6 5 spw ${⊢}\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({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)$