Axiom ax-c11

Description: Axiom ax-c11 was the original version of ax-c11n ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n could replace it. It appears as Axiom scheme C11' 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 axc11 . (Contributed by NM, 10-May-1993) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-c11	$$⊢\forall xx=y\to \left(\forall x\phi \to \forall y\phi \right)$$

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	4 0	wal	$$wff\forall xx=y$$
6		wph	$$wff\phi$$
7	6 0	wal	$$wff\forall x\phi$$
8	6 2	wal	$$wff\forall y\phi$$
9	7 8	wi	$$wff\left(\forall x\phi \to \forall y\phi \right)$$
10	5 9	wi	$$wff\left(\forall xx=y\to \left(\forall x\phi \to \forall y\phi \right)\right)$$