Theorem ax12

Description: Rederivation of Axiom ax-12 from ax12v (used only via sp ) , axc11r , and axc15 (on top of Tarski's FOL). Since this version depends on ax-13 , usage of the weaker ax12v , ax12w , ax12i are preferred. (Contributed by NM, 22-Jan-2007) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020) (Proof shortened by BJ, 4-Jul-2021) (New usage is discouraged.)

	Ref	Expression
Assertion	ax12	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axc11r	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 𝜑 ) )
2		ala1	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
3	1 2	syl6	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
4	3	a1d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
5		sp	⊢ ( ∀ 𝑦 𝜑 → 𝜑 )
6		axc15	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
7	5 6	syl7	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
8	4 7	pm2.61i	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )