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 2130) but is used as an auxiliary axiom scheme to achieve metalogical completeness. Use its weak version alcomimw 2042 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 1535	. . 3 wff ∀𝑦𝜑
4		vx	. . 3 setvar 𝑥
5	3, 4	wal 1535	. 2 wff ∀𝑥∀𝑦𝜑
6	1, 4	wal 1535	. . 3 wff ∀𝑥𝜑
7	6, 2	wal 1535	. 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  2332  hbae  2439  hbaltg  35771  bj-hbalt  36647  bj-nnflemaa  36728  bj-nfald  37103  hbae-o  38859  axc711  38870  axc5c711  38874  ax12indalem  38901  ax12inda2ALT  38902  pm11.71  44366  axc5c4c711  44370  axc11next  44375  hbalg  44526  hbalgVD  44876  hbexgVD  44877  ichal  47340