Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralcom | Structured version Visualization version GIF version |
Description: Commutation of restricted universal quantifiers. See ralcom2 3288 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3288 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Ref | Expression |
---|---|
ralcom | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancomst 468 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) | |
2 | 1 | 2albii 1828 | . . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) |
3 | alcom 2161 | . . 3 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) | |
4 | 2, 3 | bitri 278 | . 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) |
5 | r2al 3123 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | |
6 | r2al 3123 | . 2 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) | |
7 | 4, 5, 6 | 3bitr4i 306 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∀wal 1541 ∈ wcel 2111 ∀wral 3062 |
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 2159 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-ral 3067 |
This theorem is referenced by: ralcom13 3284 ralrot3 3286 2reu4lem 4452 ssint 4890 iinrab2 4993 disjxun 5066 reusv3 5313 cnvpo 6165 cnvso 6166 dfpo2 6174 fununi 6473 isocnv2 7159 dfsmo2 8105 tz7.48lem 8198 ixpiin 8626 boxriin 8642 dedekind 11020 rexfiuz 14936 gcdcllem1 16083 mreacs 17186 comfeq 17234 catpropd 17237 isnsg2 18597 cntzrec 18753 oppgsubm 18779 opprirred 19745 opprsubrg 19846 rmodislmodlem 19991 rmodislmod 19992 islindf4 20825 cpmatmcllem 21639 tgss2 21908 ist1-2 22268 kgencn 22477 ptcnplem 22542 cnmptcom 22599 fbun 22761 cnflf 22923 fclsopn 22935 cnfcf 22963 isclmp 24018 isncvsngp 24070 caucfil 24204 ovolgelb 24401 dyadmax 24519 ftc1a 24958 ulmcau 25311 perpcom 26828 colinearalg 27025 uhgrvd00 27646 pthdlem2lem 27878 frgrwopregbsn 28424 phoeqi 28962 ho02i 29934 hoeq2 29936 adjsym 29938 cnvadj 29997 mddmd2 30414 cdj3lem3b 30545 mgccnv 31020 cvmlift2lem12 33012 elpotr 33499 noetasuplem4 33702 conway 33756 cofcutr 33855 fvineqsnf1 35345 poimirlem29 35570 heicant 35576 ispsubsp2 37524 fsuppind 40018 ntrclsiso 41383 ntrneiiso 41407 ntrneik2 41408 ntrneix2 41409 ntrneik3 41412 ntrneix3 41413 ntrneik13 41414 ntrneix13 41415 ntrneik4w 41416 imo72b2 41490 tratrb 41858 hbra2VD 42182 tratrbVD 42183 |
Copyright terms: Public domain | W3C validator |