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	|- ( ph <-> A. x ( x = y -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1	|- ( ph -> ( x = y -> ph ) )
2	1	alrimiv	|- ( ph -> A. x ( x = y -> ph ) )
3		exim	|- ( A. x ( x = y -> ph ) -> ( E. x x = y -> E. x ph ) )
4		ax6ev	|- E. x x = y
5		pm2.27	|- ( E. x x = y -> ( ( E. x x = y -> E. x ph ) -> E. x ph ) )
6	4 5	ax-mp	|- ( ( E. x x = y -> E. x ph ) -> E. x ph )
7		ax5e	|- ( E. x ph -> ph )
8	3 6 7	3syl	|- ( A. x ( x = y -> ph ) -> ph )
9	2 8	impbii	|- ( ph <-> A. x ( x = y -> ph ) )