Axiom ax-11 2190

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 2163) but is used as an auxiliary axiom scheme to achieve metalogical completeness. Use its weak version alcomimw 2071 when it allows to avoid dependence on ax-11 2190. (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 1566	. . 3 wff ∀𝑦𝜑
4		vx	. . 3 setvar 𝑥
5	3, 4	wal 1566	. 2 wff ∀𝑥∀𝑦𝜑
6	1, 4	wal 1566	. . 3 wff ∀𝑥𝜑
7	6, 2	wal 1566	. 2 wff ∀𝑦∀𝑥𝜑
8	5, 7	wi 4	1 wff (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

This axiom is referenced by:  alcoms  2191  alcom  2192  hbal  2200  hbald  2201  nfald  2359  hbae  2461  hbaltg  36251  bj-hbald  37248  bj-nnflemaa  37355  bj-nfald  37723  hbae-o  39623  axc711  39634  axc5c711  39638  ax12indalem  39665  ax12inda2ALT  39666  pm11.71  45055  axc5c4c711  45059  axc11next  45064  hbalg  45212  hbalgVD  45561  hbexgVD  45562  ichal  48160