Axiom ax-11 2158

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

This axiom is referenced by:  alcoms  2159  alcom  2160  hbal  2168  hbald  2169  hbsbwOLD  2173  nfald  2327  hbae  2429  hbaltg  35780  bj-hbalt  36654  bj-nnflemaa  36735  bj-nfald  37110  hbae-o  38881  axc711  38892  axc5c711  38896  ax12indalem  38923  ax12inda2ALT  38924  pm11.71  44370  axc5c4c711  44374  axc11next  44379  hbalg  44529  hbalgVD  44878  hbexgVD  44879  ichal  47451