![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralcom4 | Structured version Visualization version GIF version |
Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) |
Ref | Expression |
---|---|
ralcom4 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.21v 1899 | . . . . 5 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
2 | 1 | bicomi 216 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) |
3 | 2 | albii 1783 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) |
4 | alcom 2096 | . . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
5 | 3, 4 | bitri 267 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
6 | df-ral 3088 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
7 | df-ral 3088 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
8 | 7 | albii 1783 | . 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
9 | 5, 6, 8 | 3bitr4i 295 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∀wal 1506 ∈ wcel 2051 ∀wral 3083 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-11 2094 |
This theorem depends on definitions: df-bi 199 df-ex 1744 df-ral 3088 |
This theorem is referenced by: ralxpxfr2d 3549 uniiunlem 3946 iunss 4832 disjor 4908 trintOLD 5044 reliun 5536 idrefALT 5811 funimass4 6558 ralrnmpo 7104 findcard3 8555 kmlem12 9380 fimaxre3 11387 vdwmc2 16170 ramtlecl 16191 iunocv 20543 1stccn 21791 itg2leub 24054 mptelee 26400 nmoubi 28342 nmopub 29482 nmfnleub 29499 moel 30050 disjorf 30113 funcnv5mpt 30193 untuni 32488 elintfv 32560 heibor1lem 34562 ineleq 35087 inecmo 35088 pmapglbx 36383 ss2iundf 39401 ismnuprim 40039 iunssf 40805 setrec1lem2 44188 |
Copyright terms: Public domain | W3C validator |