![]() |
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.) (Proof shortened by Wolf Lammen, 31-Oct-2024.) |
Ref | Expression |
---|---|
ralcom4 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.21v 1935 | . . . 4 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
2 | 1 | albii 1814 | . . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) |
3 | alcom 2149 | . . 3 ⊢ (∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3052 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
5 | 2, 3, 4 | 3bitr4ri 303 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
6 | df-ral 3052 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
7 | 6 | albii 1814 | . 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
8 | 5, 7 | bitr4i 277 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1532 ∈ wcel 2099 ∀wral 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-11 2147 |
This theorem depends on definitions: df-bi 206 df-ex 1775 df-ral 3052 |
This theorem is referenced by: moelOLD 3389 ralxpxfr2d 3630 uniiunlem 4080 iunssf 5044 iunss 5045 disjor 5125 reliun 5814 idrefALT 6115 funimass4 6959 fnssintima 7366 ralrnmpo 7557 imaeqalov 7657 ralxp3f 8143 findcard3 9312 findcard3OLD 9313 ttrclss 9756 kmlem12 10197 fimaxre3 12206 vdwmc2 16976 ramtlecl 16997 iunocv 21673 1stccn 23455 itg2leub 25752 eqscut2 27833 addsuniflem 28012 mulsuniflem 28147 mptelee 28826 nmoubi 30702 nmopub 31838 nmfnleub 31855 disjorf 32499 funcnv5mpt 32585 untuni 35544 elintfv 35601 heibor1lem 37523 ineleq 38065 inecmo 38066 pmapglbx 39481 ismnuprim 44005 setrec1lem2 48470 |
Copyright terms: Public domain | W3C validator |