Axiom ax-11 2156

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

This axiom is referenced by:  alcoms  2157  alcom  2158  hbal  2166  hbald  2167  hbsbwOLD  2171  nfald  2327  hbae  2434  hbaltg  35767  bj-hbalt  36641  bj-nnflemaa  36722  bj-nfald  37097  hbae-o  38863  axc711  38874  axc5c711  38878  ax12indalem  38905  ax12inda2ALT  38906  pm11.71  44373  axc5c4c711  44377  axc11next  44382  hbalg  44532  hbalgVD  44882  hbexgVD  44883  ichal  47411