Axiom ax-9o 1159

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

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

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 991	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 991	. . . . 5 class y
5	2, 4	wceq 992	. . . 4 wff x = y
6		wph	. . . . 5 wff φ
7	6, 1	wal 990	. . . 4 wff ∀xφ
8	5, 7	wi 3	. . 3 wff (x = y → ∀xφ)
9	8, 1	wal 990	. 2 wff ∀x(x = y → ∀xφ)
10	9, 6	wi 3	1 wff (∀x(x = y → ∀xφ) → φ)

This axiom is referenced by:  ax9 1160  equid 1162  equs4 1187  equsal 1188  a4imt 1195  a4im 1196  cbv1 1199

Copyright terms: Public domain