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 2147
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 2119) but is used as an auxiliary axiom scheme to achieve metalogical completeness. Use its weak version alcomiw 2039 when it allows to avoid dependence on ax-11 2147. (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 1532 . . 3 wff 𝑦𝜑
4 vx . . 3 setvar 𝑥
53, 4wal 1532 . 2 wff 𝑥𝑦𝜑
61, 4wal 1532 . . 3 wff 𝑥𝜑
76, 2wal 1532 . 2 wff 𝑦𝑥𝜑
85, 7wi 4 1 wff (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  alcoms  2148  alcom  2149  hbal  2157  hbald  2158  hbsbwOLD  2162  nfald  2317  hbae  2426  hbaltg  35397  bj-hbalt  36152  bj-nnflemaa  36233  bj-nfald  36610  hbae-o  38369  axc711  38380  axc5c711  38384  ax12indalem  38411  ax12inda2ALT  38412  pm11.71  43828  axc5c4c711  43832  axc11next  43837  hbalg  43988  hbalgVD  44338  hbexgVD  44339  ichal  46800
  Copyright terms: Public domain W3C validator