Axiom ax-11d

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

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

Detailed syntax breakdown

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