Axiom ax-11 2154

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

This axiom is referenced by:  alcoms  2155  alcom  2156  hbal  2164  hbald  2165  hbsbwOLD  2169  nfald  2326  hbae  2433  hbaltg  35788  bj-hbalt  36663  bj-nnflemaa  36744  bj-nfald  37119  hbae-o  38884  axc711  38895  axc5c711  38899  ax12indalem  38926  ax12inda2ALT  38927  pm11.71  44392  axc5c4c711  44396  axc11next  44401  hbalg  44552  hbalgVD  44902  hbexgVD  44903  ichal  47390