![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexlimiva | Structured version Visualization version Unicode version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) |
Ref | Expression |
---|---|
rexlimiva.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rexlimiva |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimiva.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 440 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexlimiv 2885 |
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 1680 ax-4 1693 ax-5 1769 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-ral 2754 df-rex 2755 |
This theorem is referenced by: rexraleqim 3177 unon 6685 tfrlem16 7137 oawordeulem 7281 nneob 7379 ominf 7810 unfilem1 7861 pwfi 7895 fival 7952 elfi2 7954 fi0 7960 fiin 7962 finnum 8408 dif1card 8467 fseqenlem2 8482 dfac8alem 8486 alephfp 8565 cflim2 8719 isfin1-3 8842 fin67 8851 isfin7-2 8852 axdc3lem 8906 axdc3lem2 8907 iunfo 8990 iundom2g 8991 winainflem 9144 rankcf 9228 map2psrpr 9560 supsrlem 9561 1re 9668 00id 9834 addid1 9839 om2uzrani 12198 uzrdgfni 12204 wrdf 12709 rexanuz 13457 r19.2uz 13463 fsum2dlem 13880 fsumcom2 13884 fprod2dlem 14083 fprodcom2 14087 0dvds 14372 modprm0 14805 cshwsidrepsw 15113 psgndiflemA 19218 ppttop 20071 epttop 20073 neips 20178 lmmo 20445 2ndctop 20511 2ndcsep 20523 fbncp 20903 fgcl 20942 filuni 20949 tgioo 21863 zcld 21880 elovolm 22477 nulmbl2 22539 ellimc3 22883 limcflf 22885 pilem3 23458 pilem3OLD 23459 perfect 24208 2vmadivsum 24428 selberg3lem2 24445 selberg4 24448 pntrsumbnd2 24454 pntrlog2bndlem3 24466 pntrlog2bndlem4 24467 pntpbnd 24475 pnt3 24499 axcontlem12 25054 axcont 25055 eleclclwwlkn 25610 frgrareggt1 25893 norm1exi 26952 nmcexi 27728 lnconi 27735 pjssdif1i 27877 stri 27959 hstri 27967 stcltrthi 27980 shatomici 28060 dispcmp 28735 isrnmeas 29071 dya2iocucvr 29155 sxbrsigalem1 29156 eulerpartlemt 29253 bnj1398 29892 bnj1498 29919 mthmblem 30267 trpredlem1 30517 elno 30582 noreson 30596 mblfinlem3 32024 ismblfin 32026 volsupnfl 32030 dvtanlemOLD 32036 itg2addnclem 32038 itg2addnc 32041 cover2 32085 prtlem16 32486 rexzrexnn0 35692 isnumbasgrplem2 36008 dgraalem 36052 dgraalemOLD 36053 rp-isfinite5 36207 islptre 37737 stirlinglem13 37986 stirlinglem14 37987 stirling 37989 etransc 38187 perfectALTV 38883 tgblthelfgott 38946 tgoldbach 38949 issn 39035 uhgr3cyclex 39923 2zlidl 40207 2zrngamgm 40212 ply1mulgsumlem1 40451 ply1mulgsumlem2 40452 lincsumcl 40497 lincscmcl 40498 ellcoellss 40501 |
Copyright terms: Public domain | W3C validator |