Axiom ax-wl-13v

Description: A version of ax13v 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 . 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	$$⊢\neg \forall xx=y\to \left(y=z\to \forall xy=z\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1	0	cv	$$setvarx$$
2		vy	$$setvary$$
3	2	cv	$$setvary$$
4	1 3	wceq	$$wffx=y$$
5	4 0	wal	$$wff\forall xx=y$$
6	5	wn	$$wff\neg \forall xx=y$$
7		vz	$$setvarz$$
8	7	cv	$$setvarz$$
9	3 8	wceq	$$wffy=z$$
10	9 0	wal	$$wff\forall xy=z$$
11	9 10	wi	$$wff\left(y=z\to \forall xy=z\right)$$
12	6 11	wi	$$wff\left(\neg \forall xx=y\to \left(y=z\to \forall xy=z\right)\right)$$