Axiom ax-11d

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

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