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

Axiom ax-wl-11v 35504
Description: Version of ax-11 2160 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2160. It will later be converted into a theorem directly based on ax-11 2160. (Contributed by Wolf Lammen, 28-Jun-2019.)
Assertion
Ref Expression
ax-wl-11v (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Axiom ax-wl-11v
StepHypRef Expression
1 wph . . . 4 wff 𝜑
2 vy . . . 4 setvar 𝑦
31, 2wal 1541 . . 3 wff 𝑦𝜑
4 vx . . 3 setvar 𝑥
53, 4wal 1541 . 2 wff 𝑥𝑦𝜑
61, 4wal 1541 . . 3 wff 𝑥𝜑
76, 2wal 1541 . 2 wff 𝑦𝑥𝜑
85, 7wi 4 1 wff (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  wl-ax11-lem3  35507  wl-ax11-lem6  35510
  Copyright terms: Public domain W3C validator