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	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1	0	cv	⊢ 𝑥
2		vy	⊢ 𝑦
3	2	cv	⊢ 𝑦
4	1 3	wceq	⊢ 𝑥 = 𝑦
5	4 0	wal	⊢ ∀ 𝑥 𝑥 = 𝑦
6	5	wn	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦
7		vz	⊢ 𝑧
8	7	cv	⊢ 𝑧
9	3 8	wceq	⊢ 𝑦 = 𝑧
10	9 0	wal	⊢ ∀ 𝑥 𝑦 = 𝑧
11	9 10	wi	⊢ ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 )
12	6 11	wi	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )