Axiom ax-9o 1125

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

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

Assertion

Ref	Expression
ax-9o	|- (A.x(x = y -> A.xph) -> ph)

Detailed syntax breakdown of Axiom ax-9o

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 set x
2	1	cv 957	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 957	. . . . 5 class y
5	2, 4	wceq 958	. . . 4 wff x = y
6		wph	. . . . 5 wff ph
7	6, 1	wal 956	. . . 4 wff A.xph
8	5, 7	wi 3	. . 3 wff (x = y -> A.xph)
9	8, 1	wal 956	. 2 wff A.x(x = y -> A.xph)
10	9, 6	wi 3	1 wff (A.x(x = y -> A.xph) -> ph)

This axiom is referenced by:  ax9 1126  equid 1128  equs4 1152  equsal 1153  a4imt 1160  a4im 1161  cbv1 1164

Copyright terms: Public domain