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

Axiom ax-wl-11v 28538
Description: Version of ax-11 1782 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 1782. It will later be converted into a theorem directly based on ax-11 1782. (Contributed by Wolf Lammen, 28-Jun-2019.)
Assertion
Ref Expression
ax-wl-11v  |-  ( A. x A. y ph  ->  A. y A. x ph )
Distinct variable group:    x, y
Allowed substitution hints:    ph( x, y)

Detailed syntax breakdown of Axiom ax-wl-11v
StepHypRef Expression
1 wph . . . 4  wff  ph
2 vy . . . 4  setvar  y
31, 2wal 1368 . . 3  wff  A. y ph
4 vx . . 3  setvar  x
53, 4wal 1368 . 2  wff  A. x A. y ph
61, 4wal 1368 . . 3  wff  A. x ph
76, 2wal 1368 . 2  wff  A. y A. x ph
85, 7wi 4 1  wff  ( A. x A. y ph  ->  A. y A. x ph )
Colors of variables: wff setvar class
This axiom is referenced by:  wl-ax11-lem3  28541  wl-ax11-lem6  28544
  Copyright terms: Public domain W3C validator