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	|- ( ph <-> A. y ( y = x -> A. x ( x = y -> ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax12v	|- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
2	1	equcoms	|- ( y = x -> ( ph -> A. x ( x = y -> ph ) ) )
3	2	com12	|- ( ph -> ( y = x -> A. x ( x = y -> ph ) ) )
4	3	alrimiv	|- ( ph -> A. y ( y = x -> A. x ( x = y -> ph ) ) )
5		sp	|- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
6	5	com12	|- ( x = y -> ( A. x ( x = y -> ph ) -> ph ) )
7	6	equcoms	|- ( y = x -> ( A. x ( x = y -> ph ) -> ph ) )
8	7	a2i	|- ( ( y = x -> A. x ( x = y -> ph ) ) -> ( y = x -> ph ) )
9	8	alimi	|- ( A. y ( y = x -> A. x ( x = y -> ph ) ) -> A. y ( y = x -> ph ) )
10		bj-eqs	|- ( ph <-> A. y ( y = x -> ph ) )
11	9 10	sylibr	|- ( A. y ( y = x -> A. x ( x = y -> ph ) ) -> ph )
12	4 11	impbii	|- ( ph <-> A. y ( y = x -> A. x ( x = y -> ph ) ) )