Axiom ax-wl-11v 37585

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

Assertion

Ref	Expression
ax-wl-11v	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Axiom ax-wl-11v

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vy	. . . 4 setvar 𝑦
3	1, 2	wal 1538	. . 3 wff ∀𝑦𝜑
4		vx	. . 3 setvar 𝑥
5	3, 4	wal 1538	. 2 wff ∀𝑥∀𝑦𝜑
6	1, 4	wal 1538	. . 3 wff ∀𝑥𝜑
7	6, 2	wal 1538	. 2 wff ∀𝑦∀𝑥𝜑
8	5, 7	wi 4	1 wff (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

This axiom is referenced by:  wl-ax11-lem3  37588  wl-ax11-lem6  37591