Axiom ax-11 2170

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

This axiom is referenced by:  alcoms  2171  alcom  2172  hbal  2180  hbald  2181  nfald  2339  hbae  2441  hbaltg  36046  bj-hbald  37035  bj-nnflemaa  37142  bj-nfald  37508  hbae-o  39408  axc711  39419  axc5c711  39423  ax12indalem  39450  ax12inda2ALT  39451  pm11.71  44854  axc5c4c711  44858  axc11next  44863  hbalg  45012  hbalgVD  45361  hbexgVD  45362  ichal  47953