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 | |- ( A. x A. y ph -> A. y A. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | |- x |
|
| 1 | vy | |- y |
|
| 2 | wph | |- ph |
|
| 3 | 2 1 | wal | |- A. y ph |
| 4 | 3 0 | wal | |- A. x A. y ph |
| 5 | 2 0 | wal | |- A. x ph |
| 6 | 5 1 | wal | |- A. y A. x ph |
| 7 | 4 6 | wi | |- ( A. x A. y ph -> A. y A. x ph ) |