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 1931 | . . . . 5 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
2 | 1 | bicomi 225 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) |
3 | 2 | albii 1811 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑)) |
4 | alcom 2153 | . . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
5 | 3, 4 | bitri 276 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
6 | df-ral 3140 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑)) | |
7 | df-ral 3140 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
8 | 7 | albii 1811 | . 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
9 | 5, 6, 8 | 3bitr4i 304 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1526 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-11 2151 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-ral 3140 |
This theorem is referenced by: ralxpxfr2d 3636 uniiunlem 4058 iunss 4960 disjor 5037 reliun 5682 idrefALT 5966 funimass4 6723 ralrnmpo 7278 findcard3 8749 kmlem12 9575 fimaxre3 11575 vdwmc2 16303 ramtlecl 16324 iunocv 20753 1stccn 21999 itg2leub 24262 mptelee 26608 nmoubi 28476 nmopub 29612 nmfnleub 29629 moel 30179 disjorf 30257 funcnv5mpt 30341 untuni 32832 elintfv 32904 heibor1lem 34968 ineleq 35489 inecmo 35490 pmapglbx 36785 ss2iundf 39882 ismnuprim 40507 iunssf 41229 setrec1lem2 44719 |
Copyright terms: Public domain | W3C validator |