Metamath Proof Explorer


Theorem bj-ssblem2

Description: An instance of ax-11 proved without it. The converse may not be provable without ax-11 (since using alcomiw would require a DV on ph , x , which defeats the purpose). (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ssblem2 xyy=tx=yφyxy=tx=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 1 3 imbi12d y=zy=tx=yφz=tx=zφ
5 4 alcomiw xyy=tx=yφyxy=tx=yφ