Theorem ralrimi 2857

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 2853. (Revised by Wolf Lammen, 4-Dec-2019.)

Hypotheses

Ref	Expression
ralrimi.1
ralrimi.2

Assertion

Ref	Expression
ralrimi

Proof of Theorem ralrimi

Step	Hyp	Ref	Expression
1		ralrimi.1	. . 3
2	1	nfri 1874	. 2
3		ralrimi.2	. 2
4	2, 3	hbralrimi 2853	1

Syntax hints:  ->wi 4  F/wnf 1616  e.wcel 1818  A.wral 2807

This theorem is referenced by:  ralimdaa  2859  ralrimivOLD  2870  reximdai  2926  rexlimd2  2940  rexlimdOLD  2942  r19.12  2983  r19.29af2OLD  2996  r19.37  3006  ralcom2  3022  2rmorex  3304  iineq2d  4351  disjxiun  4449  mpteq2da  4537  reusv6OLD  4663  mpteqb  5970  fmptdf  6056  eusvobj2  6289  zfrep6  6768  tfr3  7087  tz7.49  7129  mapxpen  7703  dfac2  8532  hsmexlem4  8830  axcc3  8839  domtriomlem  8843  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  ac6num  8880  dedekind  9765  dedekindle  9766  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  mreexexd  15045  cpmatmcllem  19219  ptcnplem  20122  xkocnv  20315  cfilucfilOLD  21072  cfilucfil  21073  itg2splitlem  22155  itg2split  22156  itgeq1f  22178  mptelee  24198  foresf1o  27403  funimass4f  27474  fcomptf  27503  offval2f  27506  funcnvmptOLD  27509  funcnvmpt  27510  isarchiofld  27807  reff  27842  locfinreflem  27843  esumeq12dvaf  28044  esumel  28058  esumf1o  28061  esumc  28062  esummono  28066  gsumesum  28067  esumlub  28068  esumlef  28070  esumfsup  28076  esumpinfval  28079  esumpinfsum  28083  measinblem  28191  voliune  28201  volmeas  28203  oms0  28266  dstrvprob  28410  untsucf  29082  trpredmintr  29314  wfrlem4  29346  frrlem4  29390  cover2  30204  upixp  30220  indexdom  30225  filbcmb  30231  sdclem2  30235  eq0rabdioph  30710  eqrabdioph  30711  setindtr  30966  rzalf  31392  fnchoice  31404  refsumcn  31405  rfcnnnub  31411  refsum2cnlem1  31412  ssfiunibd  31509  fprodcllemf  31591  mccl  31606  climsuse  31614  mullimc  31622  mullimcf  31629  limcrecl  31635  limsupre  31647  limcleqr  31650  addlimc  31654  0ellimcdiv  31655  limclner  31657  cncficcgt0  31691  cncfioobd  31700  cncfcompt2  31702  dvmptfprodlem  31741  dvnprodlem1  31743  iblsplitf  31769  stoweidlem5  31787  stoweidlem16  31798  stoweidlem18  31800  stoweidlem21  31803  stoweidlem26  31808  stoweidlem27  31809  stoweidlem28  31810  stoweidlem29  31811  stoweidlem31  31813  stoweidlem34  31816  stoweidlem36  31818  stoweidlem41  31823  stoweidlem42  31824  stoweidlem44  31826  stoweidlem45  31827  stoweidlem48  31830  stoweidlem51  31833  stoweidlem55  31837  stoweidlem59  31841  stoweidlem60  31842  stoweidlem62  31844  wallispilem3  31849  stirlinglem5  31860  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem31  31920  fourierdlem39  31928  fourierdlem68  31957  fourierdlem71  31960  fourierdlem73  31962  fourierdlem77  31966  fourierdlem80  31969  fourierdlem83  31972  fourierdlem87  31976  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem113  32002  etransclem32  32049  aacllem  33216  iunconlem2  33735  bnj1379  33889  bnj1204  34068  bnj1388  34089  bnj1417  34097  bnj1489  34112  bj-rabbida  34486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-ral 2812