Axiom ax-11 2194

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

This axiom is used by:  alcoms  2195  alcom  2196  hbal  2204  hbald  2205  nfald  2360  hbae  2462  hbaltg  36369  bj-hbald  37397  bj-nnflemaa  37504  bj-nfald  37872  findcard4  38448  hbae-o  39761  axc711  39772  axc5c711  39776  ax12indalem  39803  ax12inda2ALT  39804  pm11.71  45206  axc5c4c711  45210  axc11next  45215  hbalg  45363  hbalgVD  45712  hbexgVD  45713  ichal  48351