Metamath Proof Explorer


Axiom ax-c10

Description: A variant of ax6 . 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 . (Contributed by NM, 10-Jan-1993) (New usage is discouraged.)

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

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 0 wal 𝑥 𝜑
7 4 6 wi ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 )
8 7 0 wal 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 )
9 8 5 wi ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → 𝜑 )