Axiom ax-wl-13v 37516

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

Had we additionally required 𝑥 and 𝑦 be distinct, too, this theorem would have been a direct consequence of ax-5 1910. 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	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧

Detailed syntax breakdown of Axiom ax-wl-13v

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar 𝑥
2		vy	. . . . 5 setvar 𝑦
3	1, 2	weq 1962	. . . 4 wff 𝑥 = 𝑦
4	3, 1	wal 1538	. . 3 wff ∀𝑥 𝑥 = 𝑦
5	4	wn 3	. 2 wff ¬ ∀𝑥 𝑥 = 𝑦
6		vz	. . . 4 setvar 𝑧
7	2, 6	weq 1962	. . 3 wff 𝑦 = 𝑧
8	7, 1	wal 1538	. . 3 wff ∀𝑥 𝑦 = 𝑧
9	7, 8	wi 4	. 2 wff (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)
10	5, 9	wi 4	1 wff (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))

This axiom is referenced by:  wl-ax13lem1  37517