bj-eqs

Description: A lemma for substitutions, proved from Tarski's FOL. The version without DV ( x , y ) is true but requires ax-13 . The disjoint variable condition DV ( x , ph ) is necessary for both directions: consider substituting x = z for ph . (Contributed by BJ, 25-May-2021)

		Ref	Expression
	Assertion	bj-eqs	$⊢ φ \leftrightarrow \forall x (x = y \to φ)$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$⊢ φ \to (x = y \to φ)$
2	1	alrimiv	$⊢ φ \to \forall x (x = y \to φ)$
3		exim	$⊢ \forall x (x = y \to φ) \to (\exists x x = y \to \exists x φ)$
4		ax6ev	$⊢ \exists x x = y$
5		pm2.27	$⊢ \exists x x = y \to ((\exists x x = y \to \exists x φ) \to \exists x φ)$
6	4 5	ax-mp	$⊢ (\exists x x = y \to \exists x φ) \to \exists x φ$
7		ax5e	$⊢ \exists x φ \to φ$
8	3 6 7	3syl	$⊢ \forall x (x = y \to φ) \to φ$
9	2 8	impbii	$⊢ φ \leftrightarrow \forall x (x = y \to φ)$

Metamath Proof Explorer

Theorem bj-eqs

Proof