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

This axiom is referenced by:  alcoms  2194  alcom  2195  hbal  2203  hbald  2204  nfald  2362  hbae  2464  hbaltg  36160  bj-hbald  37159  bj-nnflemaa  37266  bj-nfald  37632  hbae-o  39532  axc711  39543  axc5c711  39547  ax12indalem  39574  ax12inda2ALT  39575  pm11.71  44978  axc5c4c711  44982  axc11next  44987  hbalg  45136  hbalgVD  45485  hbexgVD  45486  ichal  48077