Axiom ax-10d

Description: Distinct variable version of axc11n . (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	ax-10d	$$⊢\forall xx=y\to \forall yy=x$$

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	3 1	wceq	$$wffy=x$$
7	6 2	wal	$$wff\forall yy=x$$
8	5 7	wi	$$wff\left(\forall xx=y\to \forall yy=x\right)$$