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

Proof

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