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	⊢ ( 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → 𝜑 ) )
2	1	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
3		exim	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝜑 ) )
4		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑦
5		pm2.27	⊢ ( ∃ 𝑥 𝑥 = 𝑦 → ( ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝜑 ) → ∃ 𝑥 𝜑 ) )
6	4 5	ax-mp	⊢ ( ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝜑 ) → ∃ 𝑥 𝜑 )
7		ax5e	⊢ ( ∃ 𝑥 𝜑 → 𝜑 )
8	3 6 7	3syl	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 )
9	2 8	impbii	⊢ ( 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )

Metamath Proof Explorer

Theorem bj-eqs

Proof