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 1947 | . . . . 5 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
2 | 1 | bicomi 227 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) |
3 | 2 | albii 1827 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) |
4 | alcom 2162 | . . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
5 | 3, 4 | bitri 278 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
6 | df-ral 3056 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
7 | df-ral 3056 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
8 | 7 | albii 1827 | . 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
9 | 5, 6, 8 | 3bitr4i 306 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1541 ∈ wcel 2112 ∀wral 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-11 2160 |
This theorem depends on definitions: df-bi 210 df-ex 1788 df-ral 3056 |
This theorem is referenced by: moel 3325 ralxpxfr2d 3543 uniiunlem 3985 iunssf 4939 iunss 4940 disjor 5019 reliun 5671 idrefALT 5958 funimass4 6755 ralrnmpo 7326 findcard3 8892 kmlem12 9740 fimaxre3 11743 vdwmc2 16495 ramtlecl 16516 iunocv 20597 1stccn 22314 itg2leub 24586 mptelee 26940 nmoubi 28807 nmopub 29943 nmfnleub 29960 disjorf 30591 funcnv5mpt 30679 untuni 33317 fnssintima 33345 ralxp3f 33355 elintfv 33408 eqscut2 33686 heibor1lem 35653 ineleq 36172 inecmo 36173 pmapglbx 37469 ss2iundf 40885 ismnuprim 41526 setrec1lem2 46008 |
Copyright terms: Public domain | W3C validator |