Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-wl-13v Structured version   Visualization version   GIF version

Axiom ax-wl-13v 32354
Description: A version of ax13v 2138 with a distinctor instead of a distinct variable expression.

Had we additonally required 𝑥 and 𝑦 be distinct, too, this theorem would have been a direct consequence of ax-5 1793. 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
StepHypRef Expression
1 vx . . . . 5 setvar 𝑥
2 vy . . . . 5 setvar 𝑦
31, 2weq 1824 . . . 4 wff 𝑥 = 𝑦
43, 1wal 1472 . . 3 wff 𝑥 𝑥 = 𝑦
54wn 3 . 2 wff ¬ ∀𝑥 𝑥 = 𝑦
6 vz . . . 4 setvar 𝑧
72, 6weq 1824 . . 3 wff 𝑦 = 𝑧
87, 1wal 1472 . . 3 wff 𝑥 𝑦 = 𝑧
97, 8wi 4 . 2 wff (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)
105, 9wi 4 1 wff (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Colors of variables: wff setvar class
This axiom is referenced by:  wl-ax13lem1  32355
  Copyright terms: Public domain W3C validator