Axiom ax-9o 1123

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

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

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 955	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 955	. . . . 5 class y
5	2, 4	wceq 956	. . . 4 wff x = y
6		wph	. . . . 5 wff ph
7	6, 1	wal 954	. . . 4 wff A.xph
8	5, 7	wi 3	. . 3 wff (x = y -> A.xph)
9	8, 1	wal 954	. 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 1124  equid 1126  equs4 1150  equsal 1151  a4imt 1158  a4im 1159  cbv1 1162

Copyright terms: Public domain