Axiom ax-11 2163

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

This axiom is referenced by:  alcoms  2164  alcom  2165  hbal  2173  hbald  2174  hbsbwOLD  2178  nfald  2334  hbae  2436  hbaltg  36001  bj-hbalt  36884  bj-nnflemaa  36965  bj-nfald  37344  hbae-o  39231  axc711  39242  axc5c711  39246  ax12indalem  39273  ax12inda2ALT  39274  pm11.71  44705  axc5c4c711  44709  axc11next  44714  hbalg  44863  hbalgVD  45212  hbexgVD  45213  ichal  47779