This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 ) ) )