Axiom ax-wl-11v

Description: Version of ax-11 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 . It will later be converted into a theorem directly based on ax-11 . (Contributed by Wolf Lammen, 28-Jun-2019)

	Ref	Expression
Assertion	ax-wl-11v	$$⊢\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)$$