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. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Ref | Expression |
---|---|
ralcom | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2751 | . 2 ⊢ Ⅎ𝑦𝐴 | |
2 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | ralcomf 3077 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 |
This theorem is referenced by: ralcom4 3197 ssint 4428 iinrab2 4519 disjxun 4581 reusv3 4802 cnvpo 5590 cnvso 5591 fununi 5878 isocnv2 6481 dfsmo2 7331 ixpiin 7820 boxriin 7836 dedekind 10079 rexfiuz 13935 gcdcllem1 15059 mreacs 16142 comfeq 16189 catpropd 16192 isnsg2 17447 cntzrec 17589 oppgsubm 17615 opprirred 18525 opprsubrg 18624 islindf4 19996 cpmatmcllem 20342 tgss2 20602 ist1-2 20961 kgencn 21169 ptcnplem 21234 cnmptcom 21291 fbun 21454 cnflf 21616 fclsopn 21628 cnfcf 21656 isclmp 22705 isncvsngp 22757 caucfil 22889 ovolgelb 23055 dyadmax 23172 ftc1a 23604 ulmcau 23953 perpcom 25408 colinearalg 25590 frgrawopreg2 26578 phoeqi 27097 ho02i 28072 hoeq2 28074 adjsym 28076 cnvadj 28135 mddmd2 28552 cdj3lem3b 28683 cvmlift2lem12 30550 dfpo2 30898 elpotr 30930 poimirlem29 32608 heicant 32614 ispsubsp2 34050 ntrclsiso 37385 ntrneiiso 37409 ntrneik2 37410 ntrneix2 37411 ntrneik3 37414 ntrneix3 37415 ntrneik13 37416 ntrneix13 37417 ntrneik4w 37418 hbra2VD 38118 2reu4a 39838 uhgrvd00 40750 pthdlem2lem 40973 frgrwopreg2 41488 |
Copyright terms: Public domain | W3C validator |