Axiom ax-11

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 ) but is used as an auxiliary axiom scheme to achieve metalogical completeness. (Contributed by NM, 12-Mar-1993)

	Ref	Expression
Assertion	ax-11	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		vy	⊢ 𝑦
2		wph	⊢ 𝜑
3	2 1	wal	⊢ ∀ 𝑦 𝜑
4	3 0	wal	⊢ ∀ 𝑥 ∀ 𝑦 𝜑
5	2 0	wal	⊢ ∀ 𝑥 𝜑
6	5 1	wal	⊢ ∀ 𝑦 ∀ 𝑥 𝜑
7	4 6	wi	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )