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 x y φ y x φ

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 vy setvar y
2 wph wff φ
3 2 1 wal wff y φ
4 3 0 wal wff x y φ
5 2 0 wal wff x φ
6 5 1 wal wff y x φ
7 4 6 wi wff x y φ y x φ