Axiom ax-11d 35169

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

Assertion

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

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Axiom ax-11d

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		vy	. . 3 setvar 𝑦
3	1, 2	weq 1962	. 2 wff 𝑥 = 𝑦
4		wph	. . . 4 wff 𝜑
5	4, 2	wal 1538	. . 3 wff ∀𝑦𝜑
6	3, 4	wi 4	. . . 4 wff (𝑥 = 𝑦 → 𝜑)
7	6, 1	wal 1538	. . 3 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
8	5, 7	wi 4	. 2 wff (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
9	3, 8	wi 4	1 wff (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

This axiom is referenced by: (None)