Axiom ax-wl-11v 33361

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

Assertion

Ref	Expression
ax-wl-11v	|- ( A. x A. y ph -> A. y A. x ph )

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Detailed syntax breakdown of Axiom ax-wl-11v

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff ph
2		vy	. . . 4 setvar y
3	1, 2	wal 1481	. . 3 wff A. y ph
4		vx	. . 3 setvar x
5	3, 4	wal 1481	. 2 wff A. x A. y ph
6	1, 4	wal 1481	. . 3 wff A. x ph
7	6, 2	wal 1481	. 2 wff A. y A. x ph
8	5, 7	wi 4	1 wff ( A. x A. y ph -> A. y A. x ph )

This axiom is referenced by:  wl-ax11-lem3  33364  wl-ax11-lem6  33367