This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax12i

Description: Inference that has ax-12 (without A. y ) as its conclusion. Uses only Tarski's FOL axiom schemes. The hypotheses may be eliminable without using ax-12 in special cases. Proof similar to Lemma 16 of Tarski p. 70. (Contributed by NM, 20-May-2008)

	Ref	Expression
Hypotheses	ax12i.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	ax12i.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
Assertion	ax12i	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax12i.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		ax12i.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
3	1	biimprcd	⊢ ( 𝜓 → ( 𝑥 = 𝑦 → 𝜑 ) )
4	2 3	alrimih	⊢ ( 𝜓 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
5	1 4	biimtrdi	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )