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

Proof

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