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	$$⊢\phi \leftrightarrow \forall y\left(y=x\to \forall x\left(x=y\to \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax12v	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
2	1	equcoms	$$⊢y=x\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
3	2	com12	$$⊢\phi \to \left(y=x\to \forall x\left(x=y\to \phi \right)\right)$$
4	3	alrimiv	$$⊢\phi \to \forall y\left(y=x\to \forall x\left(x=y\to \phi \right)\right)$$
5		sp	$$⊢\forall x\left(x=y\to \phi \right)\to \left(x=y\to \phi \right)$$
6	5	com12	$$⊢x=y\to \left(\forall x\left(x=y\to \phi \right)\to \phi \right)$$
7	6	equcoms	$$⊢y=x\to \left(\forall x\left(x=y\to \phi \right)\to \phi \right)$$
8	7	a2i	$$⊢\left(y=x\to \forall x\left(x=y\to \phi \right)\right)\to \left(y=x\to \phi \right)$$
9	8	alimi	$$⊢\forall y\left(y=x\to \forall x\left(x=y\to \phi \right)\right)\to \forall y\left(y=x\to \phi \right)$$
10		bj-eqs	$$⊢\phi \leftrightarrow \forall y\left(y=x\to \phi \right)$$
11	9 10	sylibr	$$⊢\forall y\left(y=x\to \forall x\left(x=y\to \phi \right)\right)\to \phi$$
12	4 11	impbii	$$⊢\phi \leftrightarrow \forall y\left(y=x\to \forall x\left(x=y\to \phi \right)\right)$$