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	$$⊢\forall x\left(x=y\to \forall x\phi \right)\to \phi$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1	0	cv	$$setvarx$$
2		vy	$$setvary$$
3	2	cv	$$setvary$$
4	1 3	wceq	$$wffx=y$$
5		wph	$$wff\phi$$
6	5 0	wal	$$wff\forall x\phi$$
7	4 6	wi	$$wff\left(x=y\to \forall x\phi \right)$$
8	7 0	wal	$$wff\forall x\left(x=y\to \forall x\phi \right)$$
9	8 5	wi	$$wff\left(\forall x\left(x=y\to \forall x\phi \right)\to \phi \right)$$