Theorem ralrimi 2864

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

Hypotheses

Ref	Expression
ralrimi.1	|- F/ x ph
ralrimi.2	|- ( ph -> ( x e. A -> ps ) )

Assertion

Ref	Expression
ralrimi	|- ( ph -> A. x e. A ps )

Proof of Theorem ralrimi

Step	Hyp	Ref	Expression
1		ralrimi.1	. . 3 |- F/ x ph
2	1	nfri 1822	. 2 |- ( ph -> A. x ph )
3		ralrimi.2	. 2 |- ( ph -> ( x e. A -> ps ) )
4	2, 3	hbralrimi 2860	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   F/wnf 1599   e. wcel 1767   A.wral 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600  df-ral 2819

This theorem is referenced by:  ralimdaa  2866  ralrimivOLD  2877  reximdai  2933  rexlimd2  2946  rexlimdOLD  2948  r19.12  2988  r19.29af2  3000  r19.37  3010  ralcom2  3026  2rmorex  3308  iineq2d  4346  disjxiun  4444  mpteq2da  4532  reusv6OLD  4658  mpteqb  5964  fmptdf  6046  eusvobj2  6277  zfrep6  6752  tfr3  7068  tz7.49  7110  mapxpen  7683  dfac2  8511  hsmexlem4  8809  axcc3  8818  domtriomlem  8822  axdc3lem2  8831  axdc3lem4  8833  axdc4lem  8835  ac6num  8859  dedekind  9743  dedekindle  9744  fsuppmapnn0fiublem  12064  fsuppmapnn0fiub  12065  mreexexd  14903  cpmatmcllem  19014  ptcnplem  19885  xkocnv  20078  cfilucfilOLD  20835  cfilucfil  20836  itg2splitlem  21918  itg2split  21919  itgeq1f  21941  mptelee  23902  funimass4f  27175  fcomptf  27203  offval2f  27206  funcnvmptOLD  27209  funcnvmpt  27210  isarchiofld  27498  esumeq12dvaf  27712  esumel  27726  esumf1o  27729  esumc  27730  esummono  27734  gsumesum  27735  esumlub  27736  esumlef  27738  esumfsup  27744  esumpinfval  27747  esumpinfsum  27751  measinblem  27859  voliune  27869  volmeas  27871  oms0  27934  dstrvprob  28078  untsucf  28585  trpredmintr  28919  wfrlem4  28951  frrlem4  28995  cover2  29835  upixp  29851  indexdom  29856  filbcmb  29862  sdclem2  29866  eq0rabdioph  30342  eqrabdioph  30343  setindtr  30598  rzalf  30998  fnchoice  31010  refsumcn  31011  rfcnnnub  31017  refsum2cnlem1  31018  suprnmpt  31057  ssfiunibd  31114  icoiccdif  31156  climsuse  31178  mullimc  31186  mullimcf  31193  limcrecl  31199  limsupre  31211  limcleqr  31214  addlimc  31218  0ellimcdiv  31219  limclner  31221  icccncfext  31254  cncficcgt0  31255  cncfiooicclem1  31260  cncfioobd  31264  iblsplitf  31316  stoweidlem5  31333  stoweidlem16  31344  stoweidlem18  31346  stoweidlem21  31349  stoweidlem26  31354  stoweidlem27  31355  stoweidlem28  31356  stoweidlem29  31357  stoweidlem31  31359  stoweidlem34  31362  stoweidlem36  31364  stoweidlem41  31369  stoweidlem42  31370  stoweidlem44  31372  stoweidlem45  31373  stoweidlem48  31376  stoweidlem51  31379  stoweidlem55  31383  stoweidlem59  31387  stoweidlem60  31388  stoweidlem62  31390  wallispilem3  31395  stirlinglem5  31406  fourierdlem16  31451  fourierdlem21  31456  fourierdlem22  31457  fourierdlem31  31466  fourierdlem39  31474  fourierdlem68  31503  fourierdlem71  31506  fourierdlem73  31508  fourierdlem77  31512  fourierdlem80  31515  fourierdlem83  31518  fourierdlem87  31522  fourierdlem94  31529  fourierdlem103  31538  fourierdlem104  31539  fourierdlem112  31547  fourierdlem113  31548  iunconlem2  32833  bnj1379  32986  bnj1145  33146  bnj1204  33165  bnj1388  33186  bnj1417  33194  bnj1489  33209  bj-rabbida  33585