![]() |
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 2119) but is used as an auxiliary axiom scheme to achieve metalogical completeness. Use its weak version alcomiw 2039 when it allows to avoid dependence on ax-11 2147. (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 1532 | . . 3 wff ∀𝑦𝜑 |
4 | vx | . . 3 setvar 𝑥 | |
5 | 3, 4 | wal 1532 | . 2 wff ∀𝑥∀𝑦𝜑 |
6 | 1, 4 | wal 1532 | . . 3 wff ∀𝑥𝜑 |
7 | 6, 2 | wal 1532 | . 2 wff ∀𝑦∀𝑥𝜑 |
8 | 5, 7 | wi 4 | 1 wff (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
This axiom is referenced by: alcoms 2148 alcom 2149 hbal 2157 hbald 2158 hbsbwOLD 2162 nfald 2317 hbae 2426 hbaltg 35403 bj-hbalt 36158 bj-nnflemaa 36239 bj-nfald 36616 hbae-o 38375 axc711 38386 axc5c711 38390 ax12indalem 38417 ax12inda2ALT 38418 pm11.71 43834 axc5c4c711 43838 axc11next 43843 hbalg 43994 hbalgVD 44344 hbexgVD 44345 ichal 46806 |
Copyright terms: Public domain | W3C validator |