Axiom ax-11 2146

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

This axiom is referenced by:  alcoms  2147  alcom  2148  hbal  2159  hbald  2160  hbsbw  2161  nfald  2313  hbae  2422  hbaltg  35301  bj-hbalt  36059  bj-nnflemaa  36140  bj-nfald  36518  hbae-o  38276  axc711  38287  axc5c711  38291  ax12indalem  38318  ax12inda2ALT  38319  pm11.71  43705  axc5c4c711  43709  axc11next  43714  hbalg  43865  hbalgVD  44215  hbexgVD  44216  ichal  46679