| 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 1939 | . . . 4 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
| 2 | 1 | albii 1819 | . . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) |
| 3 | alcom 2159 | . . 3 ⊢ (∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) | |
| 4 | df-ral 3062 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
| 5 | 2, 3, 4 | 3bitr4ri 304 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
| 6 | df-ral 3062 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 7 | 6 | albii 1819 | . 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
| 8 | 5, 7 | bitr4i 278 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-11 2157 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-ral 3062 |
| This theorem is referenced by: moelOLD 3405 ralxpxfr2d 3646 uniiunlem 4087 iunssf 5044 iunss 5045 disjor 5125 reliun 5826 idrefALT 6131 funimass4 6973 fnssintima 7382 ralrnmpo 7572 imaeqalov 7672 ralxp3f 8162 findcard3 9318 findcard3OLD 9319 ttrclss 9760 kmlem12 10202 fimaxre3 12214 vdwmc2 17017 ramtlecl 17038 iunocv 21699 1stccn 23471 itg2leub 25769 eqscut2 27851 addsuniflem 28034 mulsuniflem 28175 mptelee 28910 nmoubi 30791 nmopub 31927 nmfnleub 31944 disjorf 32592 funcnv5mpt 32678 untuni 35709 elintfv 35765 heibor1lem 37816 ineleq 38355 inecmo 38356 pmapglbx 39771 ismnuprim 44313 setrec1lem2 49207 |
| Copyright terms: Public domain | W3C validator |