Axiom ax-11 2157

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 2157. (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 1538	. . 3 wff ∀𝑦𝜑
4		vx	. . 3 setvar 𝑥
5	3, 4	wal 1538	. 2 wff ∀𝑥∀𝑦𝜑
6	1, 4	wal 1538	. . 3 wff ∀𝑥𝜑
7	6, 2	wal 1538	. 2 wff ∀𝑦∀𝑥𝜑
8	5, 7	wi 4	1 wff (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

This axiom is referenced by:  alcoms  2158  alcom  2159  hbal  2167  hbald  2168  hbsbwOLD  2172  nfald  2328  hbae  2435  hbaltg  35771  bj-hbalt  36645  bj-nnflemaa  36726  bj-nfald  37101  hbae-o  38867  axc711  38878  axc5c711  38882  ax12indalem  38909  ax12inda2ALT  38910  pm11.71  44369  axc5c4c711  44373  axc11next  44378  hbalg  44528  hbalgVD  44877  hbexgVD  44878  ichal  47428