Theorem ralrimi 2854

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 2850. (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 1879	. 2 |- ( ph -> A. x ph )
3		ralrimi.2	. 2 |- ( ph -> ( x e. A -> ps ) )
4	2, 3	hbralrimi 2850	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   F/wnf 1621   e. wcel 1823   A.wral 2804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859

This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622  df-ral 2809

This theorem is referenced by:  ralimdaa  2856  ralrimivOLD  2867  reximdai  2923  rexlimd2  2937  rexlimdOLD  2939  r19.12  2980  r19.29af2OLD  2993  r19.37  3003  ralcom2  3019  2rmorex  3301  iineq2d  4336  disjxiun  4436  mpteq2da  4524  reusv6OLD  4648  mpteqb  5946  fmptdf  6032  eusvobj2  6263  zfrep6  6741  tfr3  7060  tz7.49  7102  mapxpen  7676  dfac2  8502  hsmexlem4  8800  axcc3  8809  domtriomlem  8813  axdc3lem2  8822  axdc3lem4  8824  axdc4lem  8826  ac6num  8850  dedekind  9733  dedekindle  9734  fsuppmapnn0fiublem  12078  fsuppmapnn0fiub  12079  mreexexd  15137  cpmatmcllem  19386  ptcnplem  20288  xkocnv  20481  cfilucfilOLD  21238  cfilucfil  21239  itg2splitlem  22321  itg2split  22322  itgeq1f  22344  mptelee  24400  foresf1o  27602  funimass4f  27695  fcomptf  27725  aciunf1lem  27729  offval2f  27733  funcnvmptOLD  27736  funcnvmpt  27737  isarchiofld  28042  reff  28077  locfinreflem  28078  esumeq12dvaf  28260  esumgsum  28274  esumel  28276  esumf1o  28279  esumc  28280  esummono  28283  gsumesum  28288  esumlub  28289  esumlef  28291  esumfsup  28299  esumpinfval  28302  esumpinfsum  28306  esum2d  28322  sigapildsyslem  28387  measinblem  28428  voliune  28438  volmeas  28440  oms0  28505  omssubadd  28508  dstrvprob  28674  untsucf  29323  trpredmintr  29554  wfrlem4  29586  frrlem4  29630  cover2  30444  upixp  30460  indexdom  30465  filbcmb  30471  sdclem2  30475  eq0rabdioph  30949  eqrabdioph  30950  setindtr  31205  rzalf  31632  fnchoice  31644  refsumcn  31645  rfcnnnub  31651  refsum2cnlem1  31652  ssfiunibd  31748  fprodcllemf  31830  mccl  31845  climsuse  31853  mullimc  31861  mullimcf  31868  limcrecl  31874  limsupre  31886  limcleqr  31889  addlimc  31893  0ellimcdiv  31894  limclner  31896  cncficcgt0  31930  cncfioobd  31939  cncfcompt2  31941  dvmptfprodlem  31980  dvnprodlem1  31982  iblsplitf  32008  stoweidlem5  32026  stoweidlem16  32037  stoweidlem18  32039  stoweidlem21  32042  stoweidlem26  32047  stoweidlem27  32048  stoweidlem28  32049  stoweidlem29  32050  stoweidlem31  32052  stoweidlem34  32055  stoweidlem36  32057  stoweidlem41  32062  stoweidlem42  32063  stoweidlem44  32065  stoweidlem45  32066  stoweidlem48  32069  stoweidlem51  32072  stoweidlem55  32076  stoweidlem59  32080  stoweidlem60  32081  stoweidlem62  32083  wallispilem3  32088  stirlinglem5  32099  fourierdlem16  32144  fourierdlem21  32149  fourierdlem22  32150  fourierdlem31  32159  fourierdlem39  32167  fourierdlem68  32196  fourierdlem71  32199  fourierdlem73  32201  fourierdlem77  32205  fourierdlem80  32208  fourierdlem83  32211  fourierdlem87  32215  fourierdlem94  32222  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  fourierdlem113  32241  etransclem32  32288  aacllem  33604  iunconlem2  34136  bnj1379  34290  bnj1204  34469  bnj1388  34490  bnj1417  34498  bnj1489  34513  bj-rabbida  34887