Axiom ax-wl-13v 33286

Description: A version of ax13v 2247 with a distinctor instead of a distinct variable expression.

Had we additionally required x and y be distinct, too, this theorem would have been a direct consequence of ax-5 1839. So essentially this theorem states, that a distinct variable condition between set variables can be replaced with a distinctor expression. (Contributed by Wolf Lammen, 23-Jul-2021.)

Assertion

Ref	Expression
ax-wl-13v	|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )

Distinct variable groups:   x, z   y, z

Detailed syntax breakdown of Axiom ax-wl-13v

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar x
2		vy	. . . . 5 setvar y
3	1, 2	weq 1874	. . . 4 wff x = y
4	3, 1	wal 1481	. . 3 wff A. x x = y
5	4	wn 3	. 2 wff -. A. x x = y
6		vz	. . . 4 setvar z
7	2, 6	weq 1874	. . 3 wff y = z
8	7, 1	wal 1481	. . 3 wff A. x y = z
9	7, 8	wi 4	. 2 wff ( y = z -> A. x y = z )
10	5, 9	wi 4	1 wff ( -. A. x x = y -> ( y = z -> A. x y = z ) )

This axiom is referenced by:  wl-ax13lem1  33287