Axiom ax-7d

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

	Ref	Expression
Assertion	ax-7d	$$⊢\forall x\forall y\phi \to \forall y\forall x\phi$$

Detailed syntax breakdown

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