Axiom ax-11 2197

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

This axiom is used by:  alcoms  2198  alcom  2199  hbal  2207  hbald  2208  nfald  2362  hbae  2463  hbaltg  36746  bj-hbald  37758  bj-nnflemaa  37865  bj-nfald  38247  findcard4  38823  hbae-o  40151  axc711  40162  axc5c711  40166  ax12indalem  40193  ax12inda2ALT  40194  pm11.71  45571  axc5c4c711  45575  axc11next  45580  hbalg  45727  hbalgVD  46076  hbexgVD  46077  ichal  48751