Theorem ralrimi 2800

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

Syntax hints:   -> wi 4   F/wnf 1675   e. wcel 1904   A.wral 2756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676  df-ral 2761

This theorem is referenced by:  ralimdaa  2801  reximdai  2853  rexlimd2  2865  r19.12  2903  r19.37  2925  ralcom2  2941  2rmorex  3232  iineq2d  4290  disjxiun  4392  mpteq2da  4481  mpteqb  5979  fmptdf  6063  eusvobj2  6301  offval2f  6562  zfrep6  6780  wfrlem4  7057  tfr3  7135  tz7.49  7180  mapxpen  7756  dfac2  8579  hsmexlem4  8877  axcc3  8886  domtriomlem  8890  axdc3lem2  8899  axdc3lem4  8901  axdc4lem  8903  ac6num  8927  dedekind  9815  dedekindle  9816  fsuppmapnn0fiublem  12240  fsuppmapnn0fiub  12241  fprodcllemf  14089  lcmfunsnlem1  14689  lcmfunsnlem2lem1  14690  lcmfunsnlem2  14692  mreexexd  15632  cpmatmcllem  19819  ptcnplem  20713  xkocnv  20906  cfilucfil  21652  itg2splitlem  22785  itg2split  22786  itgeq1f  22808  mptelee  25004  foresf1o  28218  funimass4f  28310  fcomptf  28335  aciunf1lem  28339  funcnvmptOLD  28345  funcnvmpt  28346  isarchiofld  28654  reff  28740  locfinreflem  28741  esumeq12dvaf  28926  esumgsum  28940  esumel  28942  esumf1o  28945  esumc  28946  esummono  28949  gsumesum  28954  esumlub  28955  esumlef  28957  esumfsup  28965  esumpinfval  28968  esumpinfsum  28972  esum2d  28988  ldsysgenld  29056  sigapildsyslem  29057  ldgenpisyslem1  29059  measinblem  29116  voliune  29125  volmeas  29127  oms0  29198  omssubadd  29201  oms0OLD  29202  omssubaddOLD  29205  dstrvprob  29377  bnj1379  29714  bnj1204  29893  bnj1388  29914  bnj1417  29922  bnj1489  29937  untsucf  30409  trpredmintr  30543  frrlem4  30588  bj-rabbida  31589  cover2  32104  upixp  32120  indexdom  32125  filbcmb  32131  sdclem2  32135  eq0rabdioph  35690  eqrabdioph  35691  setindtr  35950  ss2iundf  36322  iunconlem2  37395  rzalf  37401  fnchoice  37413  refsumcn  37414  rfcnnnub  37420  refsum2cnlem1  37421  iuneq2df  37442  uzwo4  37451  ixpeq2d  37469  ixpssmapc  37477  elintd  37479  ssdf  37482  ralimralim  37488  nelrnmpt  37492  fompt  37538  rnmptssd  37544  choicefi  37552  iunmapss  37568  iunmapsn  37570  ssfiunibd  37615  xralrple2  37664  infxr  37677  mccl  37775  climsuse  37784  mullimc  37793  mullimcf  37800  limcrecl  37806  limsupre  37818  limsupreOLD  37819  limcleqr  37822  addlimc  37826  0ellimcdiv  37827  limclner  37829  cncficcgt0  37863  cncfioobd  37872  cncfcompt2  37874  dvmptfprodlem  37916  dvnprodlem1  37918  iblsplitf  37944  stoweidlem5  37977  stoweidlem16  37988  stoweidlem18  37990  stoweidlem21  37993  stoweidlem26  37998  stoweidlem27  37999  stoweidlem28  38000  stoweidlem29  38001  stoweidlem29OLD  38002  stoweidlem31  38004  stoweidlem34  38007  stoweidlem36  38009  stoweidlem41  38014  stoweidlem42  38015  stoweidlem44  38017  stoweidlem45  38018  stoweidlem48  38021  stoweidlem51  38024  stoweidlem55  38028  stoweidlem59  38032  stoweidlem60  38033  stoweidlem62  38035  stoweidlem62OLD  38036  wallispilem3  38041  stirlinglem5  38052  fourierdlem16  38097  fourierdlem21  38102  fourierdlem22  38103  fourierdlem31  38112  fourierdlem31OLD  38113  fourierdlem39  38121  fourierdlem68  38150  fourierdlem71  38153  fourierdlem73  38155  fourierdlem77  38159  fourierdlem80  38162  fourierdlem83  38165  fourierdlem87  38169  fourierdlem94  38176  fourierdlem103  38185  fourierdlem104  38186  fourierdlem112  38194  fourierdlem113  38195  etransclem32  38243  sge0revalmpt  38334  sge0fodjrnlem  38372  sge0fsummptf  38392  iundjiun  38414  meadjiun  38420  voliunsge0lem  38426  omeiunle  38457  hoicvrrex  38496  ovnsubaddlem2  38511  hoissrrn2  38518  hoidmv1lelem1  38531  hoidmvlelem3  38537  ovnhoilem1  38541  hoi2toco  38547  ovnlecvr2  38550  hspdifhsp  38556  hoiqssbllem1  38562  hoiqssbllem3  38564  hspmbllem2  38567  iccelpart  38892  lfgrnloop  39370  aacllem  41046