![]() |
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 3290 for a version without disjoint variable condition on 𝑥, 𝑦. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Ref | Expression |
---|---|
ralcom | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2934 | . 2 ⊢ Ⅎ𝑦𝐴 | |
2 | nfcv 2934 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | ralcomf 3282 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∀wral 3090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clel 2774 df-nfc 2921 df-ral 3095 |
This theorem is referenced by: ralcom13 3286 ralrot3 3288 ralcom4 3426 ssint 4728 iinrab2 4818 disjxun 4886 reusv3 5119 cnvpo 5929 cnvso 5930 fununi 6211 isocnv2 6855 dfsmo2 7729 ixpiin 8222 boxriin 8238 dedekind 10541 rexfiuz 14498 gcdcllem1 15631 mreacs 16708 comfeq 16755 catpropd 16758 isnsg2 18012 cntzrec 18153 oppgsubm 18179 opprirred 19093 opprsubrg 19197 rmodislmodlem 19326 rmodislmod 19327 islindf4 20585 cpmatmcllem 20934 tgss2 21203 ist1-2 21563 kgencn 21772 ptcnplem 21837 cnmptcom 21894 fbun 22056 cnflf 22218 fclsopn 22230 cnfcf 22258 isclmp 23308 isncvsngp 23360 caucfil 23493 ovolgelb 23688 dyadmax 23806 ftc1a 24241 ulmcau 24590 perpcom 26068 colinearalg 26263 uhgrvd00 26886 pthdlem2lem 27123 frgrwopregbsn 27729 phoeqi 28289 ho02i 29264 hoeq2 29266 adjsym 29268 cnvadj 29327 mddmd2 29744 cdj3lem3b 29875 cvmlift2lem12 31899 dfpo2 32243 elpotr 32278 noetalem3 32458 conway 32503 poimirlem29 34069 heicant 34075 ispsubsp2 35905 ntrclsiso 39331 ntrneiiso 39355 ntrneik2 39356 ntrneix2 39357 ntrneik3 39360 ntrneix3 39361 ntrneik13 39362 ntrneix13 39363 ntrneik4w 39364 hbra2VD 40039 2reu4a 42160 |
Copyright terms: Public domain | W3C validator |