Axiom ax-11 2160

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 2133) but is used as an auxiliary axiom scheme to achieve metalogical completeness. Use its weak version alcomimw 2044 when it allows to avoid dependence on ax-11 2160. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
ax-11	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

Detailed syntax breakdown of Axiom ax-11

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vy	. . . 4 setvar 𝑦
3	1, 2	wal 1539	. . 3 wff ∀𝑦𝜑
4		vx	. . 3 setvar 𝑥
5	3, 4	wal 1539	. 2 wff ∀𝑥∀𝑦𝜑
6	1, 4	wal 1539	. . 3 wff ∀𝑥𝜑
7	6, 2	wal 1539	. 2 wff ∀𝑦∀𝑥𝜑
8	5, 7	wi 4	1 wff (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

This axiom is referenced by:  alcoms  2161  alcom  2162  hbal  2170  hbald  2171  hbsbwOLD  2175  nfald  2329  hbae  2431  hbaltg  35840  bj-hbalt  36714  bj-nnflemaa  36795  bj-nfald  37170  hbae-o  38941  axc711  38952  axc5c711  38956  ax12indalem  38983  ax12inda2ALT  38984  pm11.71  44429  axc5c4c711  44433  axc11next  44438  hbalg  44587  hbalgVD  44936  hbexgVD  44937  ichal  47496