Axiom ax-wl-13v

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

Had we additionally required x and y be distinct, too, this theorem would have been a direct consequence of ax-5 . 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1	0	cv	|- x
2		vy	|- y
3	2	cv	|- y
4	1 3	wceq	|- x = y
5	4 0	wal	|- A. x x = y
6	5	wn	|- -. A. x x = y
7		vz	|- z
8	7	cv	|- z
9	3 8	wceq	|- y = z
10	9 0	wal	|- A. x y = z
11	9 10	wi	|- ( y = z -> A. x y = z )
12	6 11	wi	|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )