![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ralcom | Structured version Unicode version |
Description: Commutation of restricted quantifiers. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Ref | Expression |
---|---|
ralcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2613 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2613 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralcomf 2977 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-ex 1588 df-nf 1591 df-sb 1703 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ral 2800 |
This theorem is referenced by: ralcom4 3089 ssint 4244 iinrab2 4333 disjxun 4390 reusv3 4600 cnvpo 5475 cnvso 5476 fununi 5584 isocnv2 6123 dfsmo2 6910 ixpiin 7391 boxriin 7407 dedekind 9636 rexfiuz 12939 gcdcllem1 13799 mreacs 14700 comfeq 14749 catpropd 14752 isnsg2 15815 cntzrec 15955 oppgsubm 15981 opprirred 16902 opprsubrg 16994 islindf4 18378 tgss2 18710 ist1-2 19069 kgencn 19247 ptcnplem 19312 cnmptcom 19369 fbun 19531 cnflf 19693 fclsopn 19705 cnfcf 19733 caucfil 20912 ovolgelb 21081 dyadmax 21196 ftc1a 21627 ulmcau 21978 perpcom 23234 colinearalg 23293 phoeqi 24395 ho02i 25370 hoeq2 25372 adjsym 25374 cnvadj 25433 mddmd2 25850 cdj3lem3b 25981 cvmlift2lem12 27339 dfpo2 27701 elpotr 27730 heicant 28566 2reu4a 30153 frgrawopreg2 30784 cpmatmcllem 31183 hbra2VD 31898 ispsubsp2 33698 |
Copyright terms: Public domain | W3C validator |