Axiom ax-11 2155

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 alcomiw 2047 when it allows to avoid dependence on ax-11 2155. (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  2156  alcom  2157  hbal  2168  hbald  2169  hbsbw  2170  nfald  2322  hbae  2431  hbaltg  34717  bj-hbalt  35497  bj-nnflemaa  35578  bj-nfald  35956  hbae-o  37711  axc711  37722  axc5c711  37726  ax12indalem  37753  ax12inda2ALT  37754  pm11.71  43089  axc5c4c711  43093  axc11next  43098  hbalg  43249  hbalgVD  43599  hbexgVD  43600  ichal  46069