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 yy=txx=yφy=txx=yφ

Proof

Step Hyp Ref Expression
1 equequ1 y=zy=tz=t
2 equequ2 y=zx=yx=z
3 2 imbi1d y=zx=yφx=zφ
4 3 albidv y=zxx=yφxx=zφ
5 1 4 imbi12d y=zy=txx=yφz=txx=zφ
6 5 spw yy=txx=yφy=txx=yφ