MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-11 Structured version   Visualization version   GIF version

Axiom ax-11 2157
Description: Axiom of Quantifier Commutation. This axiom says universal quantifiers can be swapped. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Lemma 12 of [Monk2] p. 109 and Axiom C5-3 of [Monk2] p. 113. This axiom scheme is logically redundant (see ax11w 2130) but is used as an auxiliary axiom scheme to achieve metalogical completeness. Use its weak version alcomimw 2042 when it allows to avoid dependence on ax-11 2157. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
ax-11 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)

Detailed syntax breakdown of Axiom ax-11
StepHypRef Expression
1 wph . . . 4 wff 𝜑
2 vy . . . 4 setvar 𝑦
31, 2wal 1538 . . 3 wff 𝑦𝜑
4 vx . . 3 setvar 𝑥
53, 4wal 1538 . 2 wff 𝑥𝑦𝜑
61, 4wal 1538 . . 3 wff 𝑥𝜑
76, 2wal 1538 . 2 wff 𝑦𝑥𝜑
85, 7wi 4 1 wff (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  alcoms  2158  alcom  2159  hbal  2167  hbald  2168  hbsbwOLD  2172  nfald  2328  hbae  2436  hbaltg  35808  bj-hbalt  36682  bj-nnflemaa  36763  bj-nfald  37138  hbae-o  38904  axc711  38915  axc5c711  38919  ax12indalem  38946  ax12inda2ALT  38947  pm11.71  44416  axc5c4c711  44420  axc11next  44425  hbalg  44575  hbalgVD  44925  hbexgVD  44926  ichal  47453
  Copyright terms: Public domain W3C validator