Theorem ralrimi 2788

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

Syntax hints:   -> wi 4   F/wnf 1667   e. wcel 1887   A.wral 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-ral 2742

This theorem is referenced by:  ralimdaa  2790  ralrimivOLD  2801  reximdai  2856  rexlimd2  2870  rexlimdOLD  2872  r19.12  2916  r19.29af2OLD  2929  r19.37  2939  ralcom2  2955  2rmorex  3244  iineq2d  4299  disjxiun  4399  mpteq2da  4488  mpteqb  5964  fmptdf  6048  eusvobj2  6283  offval2f  6543  zfrep6  6761  wfrlem4  7039  tfr3  7117  tz7.49  7162  mapxpen  7738  dfac2  8561  hsmexlem4  8859  axcc3  8868  domtriomlem  8872  axdc3lem2  8881  axdc3lem4  8883  axdc4lem  8885  ac6num  8909  dedekind  9797  dedekindle  9798  fsuppmapnn0fiublem  12202  fsuppmapnn0fiub  12203  fprodcllemf  14012  lcmfunsnlem1  14610  lcmfunsnlem2lem1  14611  lcmfunsnlem2  14613  mreexexd  15554  cpmatmcllem  19742  ptcnplem  20636  xkocnv  20829  cfilucfil  21574  itg2splitlem  22706  itg2split  22707  itgeq1f  22729  mptelee  24925  foresf1o  28139  funimass4f  28234  fcomptf  28260  aciunf1lem  28264  funcnvmptOLD  28270  funcnvmpt  28271  isarchiofld  28580  reff  28666  locfinreflem  28667  esumeq12dvaf  28852  esumgsum  28866  esumel  28868  esumf1o  28871  esumc  28872  esummono  28875  gsumesum  28880  esumlub  28881  esumlef  28883  esumfsup  28891  esumpinfval  28894  esumpinfsum  28898  esum2d  28914  ldsysgenld  28982  sigapildsyslem  28983  ldgenpisyslem1  28985  measinblem  29042  voliune  29052  volmeas  29054  oms0  29125  omssubadd  29128  oms0OLD  29129  omssubaddOLD  29132  dstrvprob  29304  bnj1379  29642  bnj1204  29821  bnj1388  29842  bnj1417  29850  bnj1489  29865  untsucf  30337  trpredmintr  30472  frrlem4  30517  bj-rabbida  31521  cover2  32040  upixp  32056  indexdom  32061  filbcmb  32067  sdclem2  32071  eq0rabdioph  35619  eqrabdioph  35620  setindtr  35879  ss2iundf  36251  iunconlem2  37332  rzalf  37338  fnchoice  37350  refsumcn  37351  rfcnnnub  37357  refsum2cnlem1  37358  iuneq2df  37382  uzwo4  37392  ixpeq2d  37410  ixpssmapc  37418  elintd  37420  ssdf  37423  fompt  37467  rnmptssd  37473  choicefi  37481  ssfiunibd  37527  xralrple2  37577  mccl  37678  climsuse  37687  mullimc  37696  mullimcf  37703  limcrecl  37709  limsupre  37721  limsupreOLD  37722  limcleqr  37725  addlimc  37729  0ellimcdiv  37730  limclner  37732  cncficcgt0  37766  cncfioobd  37775  cncfcompt2  37777  dvmptfprodlem  37819  dvnprodlem1  37821  iblsplitf  37847  stoweidlem5  37865  stoweidlem16  37876  stoweidlem18  37878  stoweidlem21  37881  stoweidlem26  37886  stoweidlem27  37887  stoweidlem28  37888  stoweidlem29  37889  stoweidlem29OLD  37890  stoweidlem31  37892  stoweidlem34  37895  stoweidlem36  37897  stoweidlem41  37902  stoweidlem42  37903  stoweidlem44  37905  stoweidlem45  37906  stoweidlem48  37909  stoweidlem51  37912  stoweidlem55  37916  stoweidlem59  37920  stoweidlem60  37921  stoweidlem62  37923  stoweidlem62OLD  37924  wallispilem3  37929  stirlinglem5  37940  fourierdlem16  37985  fourierdlem21  37990  fourierdlem22  37991  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem39  38009  fourierdlem68  38038  fourierdlem71  38041  fourierdlem73  38043  fourierdlem77  38047  fourierdlem80  38050  fourierdlem83  38053  fourierdlem87  38057  fourierdlem94  38064  fourierdlem103  38073  fourierdlem104  38074  fourierdlem112  38082  fourierdlem113  38083  etransclem32  38131  sge0revalmpt  38220  sge0fodjrnlem  38258  sge0fsummptf  38278  iundjiun  38298  meadjiun  38304  omeiunle  38338  hoicvrrex  38378  ovnsubaddlem2  38393  hoissrrn2  38400  hoidmv1lelem1  38413  hoidmvlelem3  38419  ovnhoilem1  38423  hoi2toco  38429  ovnlecvr2  38432  hspdifhsp  38438  hoiqssbllem1  38444  hoiqssbllem3  38446  hspmbllem2  38449  iccelpart  38747  aacllem  40593