Axiom ax-c10

Description: A variant of ax6 . Axiom scheme C10' in Megill p. 448 (p. 16 of the preprint).

This axiom is obsolete and should no longer be used. It is proved above as Theorem axc10 . (Contributed by NM, 10-Jan-1993) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-c10	|- ( A. x ( x = y -> A. x ph ) -> ph )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1	0	cv	|- x
2		vy	|- y
3	2	cv	|- y
4	1 3	wceq	|- x = y
5		wph	|- ph
6	5 0	wal	|- A. x ph
7	4 6	wi	|- ( x = y -> A. x ph )
8	7 0	wal	|- A. x ( x = y -> A. x ph )
9	8 5	wi	|- ( A. x ( x = y -> A. x ph ) -> ph )