Axiom ax-11 2158

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

This axiom is referenced by:  alcoms  2159  alcom  2160  hbal  2168  hbald  2169  hbsbwOLD  2173  nfald  2327  hbae  2429  hbaltg  35795  bj-hbalt  36669  bj-nnflemaa  36750  bj-nfald  37125  hbae-o  38896  axc711  38907  axc5c711  38911  ax12indalem  38938  ax12inda2ALT  38939  pm11.71  44386  axc5c4c711  44390  axc11next  44395  hbalg  44545  hbalgVD  44894  hbexgVD  44895  ichal  47464