![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralcom | Structured version Visualization version Unicode 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 2591 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2591 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralcomf 2948 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-ex 1663 df-nf 1667 df-sb 1797 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ral 2741 |
This theorem is referenced by: ralcom4 3065 ssint 4249 iinrab2 4340 disjxun 4399 reusv3 4610 cnvpo 5373 cnvso 5374 fununi 5647 isocnv2 6220 dfsmo2 7063 ixpiin 7545 boxriin 7561 dedekind 9794 rexfiuz 13403 gcdcllem1 14466 mreacs 15557 comfeq 15604 catpropd 15607 isnsg2 16840 cntzrec 16980 oppgsubm 17006 opprirred 17923 opprsubrg 18022 islindf4 19389 cpmatmcllem 19735 tgss2 19996 ist1-2 20356 kgencn 20564 ptcnplem 20629 cnmptcom 20686 fbun 20848 cnflf 21010 fclsopn 21022 cnfcf 21050 caucfil 22246 ovolgelb 22426 dyadmax 22549 ftc1a 22982 ulmcau 23343 perpcom 24751 colinearalg 24933 frgrawopreg2 25772 phoeqi 26492 ho02i 27475 hoeq2 27477 adjsym 27479 cnvadj 27538 mddmd2 27955 cdj3lem3b 28086 cvmlift2lem12 30030 dfpo2 30388 elpotr 30420 poimirlem29 31962 heicant 31968 ispsubsp2 33305 hbra2VD 37251 2reu4a 38604 uhgrvd00 39554 |
Copyright terms: Public domain | W3C validator |