Axiom ax-c10 38887

Description: A variant of ax6 2389. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint).

This axiom is obsolete and should no longer be used. It is proved above as Theorem axc10 2390. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)

Assertion

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

Detailed syntax breakdown of Axiom ax-c10

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

This axiom is referenced by:  ax6fromc10  38897  equid1  38900  equid1ALT  38926