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 1940 | . . . . 5 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
2 | 1 | bicomi 226 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) |
3 | 2 | albii 1820 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) |
4 | alcom 2163 | . . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
5 | 3, 4 | bitri 277 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
6 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
7 | df-ral 3143 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
8 | 7 | albii 1820 | . 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
9 | 5, 6, 8 | 3bitr4i 305 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1535 ∈ wcel 2114 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-11 2161 |
This theorem depends on definitions: df-bi 209 df-ex 1781 df-ral 3143 |
This theorem is referenced by: ralxpxfr2d 3639 uniiunlem 4061 iunss 4969 disjor 5046 reliun 5689 idrefALT 5973 funimass4 6730 ralrnmpo 7289 findcard3 8761 kmlem12 9587 fimaxre3 11587 vdwmc2 16315 ramtlecl 16336 iunocv 20825 1stccn 22071 itg2leub 24335 mptelee 26681 nmoubi 28549 nmopub 29685 nmfnleub 29702 moel 30252 disjorf 30329 funcnv5mpt 30413 untuni 32935 elintfv 33007 heibor1lem 35102 ineleq 35623 inecmo 35624 pmapglbx 36920 ss2iundf 40024 ismnuprim 40650 iunssf 41372 setrec1lem2 44811 |
Copyright terms: Public domain | W3C validator |