Axiom ax-11 2162

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

This axiom is referenced by:  alcoms  2163  alcom  2164  hbal  2172  hbald  2173  hbsbwOLD  2177  nfald  2331  hbae  2433  hbaltg  35870  bj-hbalt  36746  bj-nnflemaa  36827  bj-nfald  37202  hbae-o  39022  axc711  39033  axc5c711  39037  ax12indalem  39064  ax12inda2ALT  39065  pm11.71  44514  axc5c4c711  44518  axc11next  44523  hbalg  44672  hbalgVD  45021  hbexgVD  45022  ichal  47590