| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ax-11 | Structured version Visualization version GIF version | ||
| 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 2130) but is used as an auxiliary axiom scheme to achieve metalogical completeness. Use its weak version alcomimw 2042 when it allows to avoid dependence on ax-11 2157. (Contributed by NM, 12-Mar-1993.) |
| Ref | Expression |
|---|---|
| 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 (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
| Colors of variables: wff setvar class |
| This axiom is referenced by: alcoms 2158 alcom 2159 hbal 2167 hbald 2168 hbsbwOLD 2172 nfald 2328 hbae 2436 hbaltg 35808 bj-hbalt 36682 bj-nnflemaa 36763 bj-nfald 37138 hbae-o 38904 axc711 38915 axc5c711 38919 ax12indalem 38946 ax12inda2ALT 38947 pm11.71 44416 axc5c4c711 44420 axc11next 44425 hbalg 44575 hbalgVD 44925 hbexgVD 44926 ichal 47453 |
| Copyright terms: Public domain | W3C validator |