Theorem ralrimi 2826

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

Syntax hints:   -> wi 4   F/wnf 1664   e. wcel 1869   A.wral 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-12 1906

This theorem depends on definitions:  df-bi 189  df-ex 1661  df-nf 1665  df-ral 2781

This theorem is referenced by:  ralimdaa  2828  ralrimivOLD  2839  reximdai  2895  rexlimd2  2909  rexlimdOLD  2911  r19.12  2955  r19.29af2OLD  2968  r19.37  2978  ralcom2  2994  2rmorex  3277  iineq2d  4318  disjxiun  4418  mpteq2da  4507  mpteqb  5978  fmptdf  6061  eusvobj2  6296  offval2f  6555  zfrep6  6773  wfrlem4  7045  tfr3  7123  tz7.49  7168  mapxpen  7742  dfac2  8563  hsmexlem4  8861  axcc3  8870  domtriomlem  8874  axdc3lem2  8883  axdc3lem4  8885  axdc4lem  8887  ac6num  8911  dedekind  9799  dedekindle  9800  fsuppmapnn0fiublem  12203  fsuppmapnn0fiub  12204  fprodcllemf  14005  lcmfunsnlem1  14603  lcmfunsnlem2lem1  14604  lcmfunsnlem2  14606  mreexexd  15547  cpmatmcllem  19734  ptcnplem  20628  xkocnv  20821  cfilucfil  21566  itg2splitlem  22698  itg2split  22699  itgeq1f  22721  mptelee  24917  foresf1o  28132  funimass4f  28230  fcomptf  28256  aciunf1lem  28260  funcnvmptOLD  28266  funcnvmpt  28267  isarchiofld  28582  reff  28668  locfinreflem  28669  esumeq12dvaf  28854  esumgsum  28868  esumel  28870  esumf1o  28873  esumc  28874  esummono  28877  gsumesum  28882  esumlub  28883  esumlef  28885  esumfsup  28893  esumpinfval  28896  esumpinfsum  28900  esum2d  28916  ldsysgenld  28984  sigapildsyslem  28985  ldgenpisyslem1  28987  measinblem  29044  voliune  29054  volmeas  29056  oms0  29127  omssubadd  29130  oms0OLD  29131  omssubaddOLD  29134  dstrvprob  29306  bnj1379  29644  bnj1204  29823  bnj1388  29844  bnj1417  29852  bnj1489  29867  untsucf  30339  trpredmintr  30473  frrlem4  30518  bj-rabbida  31484  cover2  31960  upixp  31976  indexdom  31981  filbcmb  31987  sdclem2  31991  eq0rabdioph  35544  eqrabdioph  35545  setindtr  35805  ss2iundf  36117  iunconlem2  37199  rzalf  37205  fnchoice  37217  refsumcn  37218  rfcnnnub  37224  refsum2cnlem1  37225  iuneq2df  37249  uzwo4  37260  ixpeq2d  37279  fompt  37323  rnmptssd  37329  ssfiunibd  37375  mccl  37504  climsuse  37513  mullimc  37522  mullimcf  37529  limcrecl  37535  limsupre  37547  limsupreOLD  37548  limcleqr  37551  addlimc  37555  0ellimcdiv  37556  limclner  37558  cncficcgt0  37592  cncfioobd  37601  cncfcompt2  37603  dvmptfprodlem  37645  dvnprodlem1  37647  iblsplitf  37673  stoweidlem5  37691  stoweidlem16  37702  stoweidlem18  37704  stoweidlem21  37707  stoweidlem26  37712  stoweidlem27  37713  stoweidlem28  37714  stoweidlem29  37715  stoweidlem29OLD  37716  stoweidlem31  37718  stoweidlem34  37721  stoweidlem36  37723  stoweidlem41  37728  stoweidlem42  37729  stoweidlem44  37731  stoweidlem45  37732  stoweidlem48  37735  stoweidlem51  37738  stoweidlem55  37742  stoweidlem59  37746  stoweidlem60  37747  stoweidlem62  37749  stoweidlem62OLD  37750  wallispilem3  37755  stirlinglem5  37766  fourierdlem16  37811  fourierdlem21  37816  fourierdlem22  37817  fourierdlem31  37826  fourierdlem31OLD  37827  fourierdlem39  37835  fourierdlem68  37864  fourierdlem71  37867  fourierdlem73  37869  fourierdlem77  37873  fourierdlem80  37876  fourierdlem83  37879  fourierdlem87  37883  fourierdlem94  37890  fourierdlem103  37899  fourierdlem104  37900  fourierdlem112  37908  fourierdlem113  37909  etransclem32  37957  sge0revalmpt  38014  sge0fodjrnlem  38052  iundjiun  38083  meadjiun  38089  omeiunle  38123  hoicvrrex  38159  ovnsubaddlem2  38174  iccelpart  38465  aacllem  39846