Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-7d Structured version   Visualization version   GIF version

Axiom ax-7d 30240
Description: Distinct variable version of ax-11 1971. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
ax-7d (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

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