![]() |
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 14501 gcdcllem1 15637 mreacs 16715 comfeq 16762 catpropd 16765 isnsg2 18019 cntzrec 18160 oppgsubm 18186 opprirred 19100 opprsubrg 19204 rmodislmodlem 19333 rmodislmod 19334 islindf4 20592 cpmatmcllem 20941 tgss2 21210 ist1-2 21570 kgencn 21779 ptcnplem 21844 cnmptcom 21901 fbun 22063 cnflf 22225 fclsopn 22237 cnfcf 22265 isclmp 23315 isncvsngp 23367 caucfil 23500 ovolgelb 23695 dyadmax 23813 ftc1a 24248 ulmcau 24597 perpcom 26081 colinearalg 26276 uhgrvd00 26899 pthdlem2lem 27136 frgrwopregbsn 27742 phoeqi 28302 ho02i 29277 hoeq2 29279 adjsym 29281 cnvadj 29340 mddmd2 29757 cdj3lem3b 29888 cvmlift2lem12 31903 dfpo2 32247 elpotr 32282 noetalem3 32462 conway 32507 poimirlem29 34073 heicant 34079 ispsubsp2 35909 ntrclsiso 39335 ntrneiiso 39359 ntrneik2 39360 ntrneix2 39361 ntrneik3 39364 ntrneix3 39365 ntrneik13 39366 ntrneix13 39367 ntrneik4w 39368 hbra2VD 40043 2reu4a 42164 |
Copyright terms: Public domain | W3C validator |