Metamath Proof Explorer


Theorem bj-sb

Description: A weak variant of sbid2 not requiring ax-13 nor ax-10 . On top of Tarski's FOL, one implication requires only ax12v , and the other requires only sp . (Contributed by BJ, 25-May-2021)

Ref Expression
Assertion bj-sb φ y y = x x x = y φ

Proof

Step Hyp Ref Expression
1 ax12v x = y φ x x = y φ
2 1 equcoms y = x φ x x = y φ
3 2 com12 φ y = x x x = y φ
4 3 alrimiv φ y y = x x x = y φ
5 sp x x = y φ x = y φ
6 5 com12 x = y x x = y φ φ
7 6 equcoms y = x x x = y φ φ
8 7 a2i y = x x x = y φ y = x φ
9 8 alimi y y = x x x = y φ y y = x φ
10 bj-eqs φ y y = x φ
11 9 10 sylibr y y = x x x = y φ φ
12 4 11 impbii φ y y = x x x = y φ