Axiom ax-9o 1792

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

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

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 1614	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 1614	. . . . 5 class y
5	2, 4	wceq 1615	. . . 4 wff x = y
6		wph	. . . . 5 wff ph
7	6, 1	wal 1613	. . . 4 wff A.xph
8	5, 7	wi 3	. . 3 wff (x = y -> A.xph)
9	8, 1	wal 1613	. 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 1793  equid 1795  equs4 1820  equsal 1821  a4imt 1829  a4im 1830  cbv1 1833

Copyright terms: Public domain