Axiom ax-10d

Description: Distinct variable version of axc11n . (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	ax-10d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑦 = 𝑥 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1	0	cv	⊢ 𝑥
2		vy	⊢ 𝑦
3	2	cv	⊢ 𝑦
4	1 3	wceq	⊢ 𝑥 = 𝑦
5	4 0	wal	⊢ ∀ 𝑥 𝑥 = 𝑦
6	3 1	wceq	⊢ 𝑦 = 𝑥
7	6 2	wal	⊢ ∀ 𝑦 𝑦 = 𝑥
8	5 7	wi	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑦 = 𝑥 )