Axiom ax-9o 1127

Description: A variant of ax-9 969. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint).

This axiom is redundant, as shown by theorem ax9o 1126.

Assertion

Ref	Expression
ax-9o	⊢ (∀x(x = y → ∀xφ) → φ)

Detailed syntax breakdown of Axiom ax-9o

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 set x
2	1	cv 959	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 959	. . . . 5 class y
5	2, 4	wceq 960	. . . 4 wff x = y
6		wph	. . . . 5 wff φ
7	6, 1	wal 958	. . . 4 wff ∀xφ
8	5, 7	wi 3	. . 3 wff (x = y → ∀xφ)
9	8, 1	wal 958	. 2 wff ∀x(x = y → ∀xφ)
10	9, 6	wi 3	1 wff (∀x(x = y → ∀xφ) → φ)

This axiom is referenced by:  ax9 1128  equid 1130  equs4 1154  equsal 1155  a4imt 1162  a4im 1163  cbv1 1166

Copyright terms: Public domain