![]() |
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 1937 | . . . 4 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
2 | 1 | albii 1816 | . . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) |
3 | alcom 2157 | . . 3 ⊢ (∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3060 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
5 | 2, 3, 4 | 3bitr4ri 304 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
6 | df-ral 3060 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
7 | 6 | albii 1816 | . 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
8 | 5, 7 | bitr4i 278 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 ∈ wcel 2106 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-11 2155 |
This theorem depends on definitions: df-bi 207 df-ex 1777 df-ral 3060 |
This theorem is referenced by: moelOLD 3403 ralxpxfr2d 3646 uniiunlem 4097 iunssf 5049 iunss 5050 disjor 5130 reliun 5829 idrefALT 6134 funimass4 6973 fnssintima 7382 ralrnmpo 7572 imaeqalov 7672 ralxp3f 8161 findcard3 9316 findcard3OLD 9317 ttrclss 9758 kmlem12 10200 fimaxre3 12212 vdwmc2 17013 ramtlecl 17034 iunocv 21717 1stccn 23487 itg2leub 25784 eqscut2 27866 addsuniflem 28049 mulsuniflem 28190 mptelee 28925 nmoubi 30801 nmopub 31937 nmfnleub 31954 disjorf 32599 funcnv5mpt 32685 untuni 35689 elintfv 35746 heibor1lem 37796 ineleq 38336 inecmo 38337 pmapglbx 39752 ismnuprim 44290 setrec1lem2 48919 |
Copyright terms: Public domain | W3C validator |