Axiom ax-11 2193

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

This axiom is used by:  alcoms  2194  alcom  2195  hbal  2203  hbald  2204  nfald  2358  hbae  2460  hbaltg  36611  bj-hbald  37623  bj-nnflemaa  37730  bj-nfald  38099  findcard4  38675  hbae-o  40003  axc711  40014  axc5c711  40018  ax12indalem  40045  ax12inda2ALT  40046  pm11.71  45423  axc5c4c711  45427  axc11next  45432  hbalg  45580  hbalgVD  45929  hbexgVD  45930  ichal  48590