Metamath Proof Explorer


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 ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )