Theorem ralrimi 3244

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). For a version based on fewer axioms see ralrimiv 3132. (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3131. (Revised by Wolf Lammen, 4-Dec-2019.)

Hypotheses

Ref	Expression
ralrimi.1	⊢ Ⅎ𝑥𝜑
ralrimi.2	⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))

Assertion

Ref	Expression
ralrimi	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralrimi

Step	Hyp	Ref	Expression
1		ralrimi.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nf5ri 2196	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		ralrimi.2	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	2, 3	hbralrimi 3131	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-ral 3053

This theorem is referenced by:  ralrimia  3245  ralimdaa  3247  reximdai  3248  r19.37  3249  rexlimd2  3252  r19.12  3298  ralcom2  3361  rabbidaOLD  3461  2rmorex  3742  iineq2d  4996  disjxiun  5121  rnmpt0f  6237  fnmptd  6684  mpteqb  7010  fmptdf  7112  eusvobj2  7402  offval2f  7691  zfrep6  7958  frrlem4  8293  wfrlem4OLD  8331  tfr3  8418  tz7.49  8464  mapxpen  9162  dfac2b  10150  hsmexlem4  10448  axcc3  10457  domtriomlem  10461  axdc3lem2  10470  axdc3lem4  10472  axdc4lem  10474  ac6num  10498  dedekind  11403  dedekindle  11404  fsuppmapnn0fiublem  14013  fsuppmapnn0fiub  14014  fprodcllemf  15979  lcmfunsnlem1  16661  lcmfunsnlem2lem1  16662  lcmfunsnlem2  16664  mreexexd  17665  cpmatmcllem  22661  ptcnplem  23564  xkocnv  23757  cfilucfil  24503  cncfcompt2  24857  itg2splitlem  25706  itg2split  25707  itgeq1fOLD  25730  mptelee  28879  lfgrnloop  29109  foresf1o  32490  iinabrex  32555  funimass4f  32620  fcomptf  32641  aciunf1lem  32645  funcnvmpt  32650  fnpreimac  32654  prodindf  32845  isarchiofld  33344  reff  33875  locfinreflem  33876  zarclsiin  33907  zarcmplem  33917  esumeq12dvaf  34067  esumgsum  34081  esumel  34083  esumf1o  34086  esumc  34087  esummono  34090  gsumesum  34095  esumlub  34096  esumlef  34098  esumfsup  34106  esumpinfval  34109  esumpinfsum  34113  esum2d  34129  ldsysgenld  34196  sigapildsyslem  34197  ldgenpisyslem1  34199  measinblem  34256  voliune  34265  volmeas  34267  oms0  34334  omssubadd  34337  dstrvprob  34509  bnj1379  34866  bnj1204  35048  bnj1388  35069  bnj1417  35077  bnj1489  35092  untsucf  35732  domalom  37427  fvineqsneq  37435  cover2  37744  upixp  37758  indexdom  37763  filbcmb  37769  sdclem2  37771  eq0rabdioph  42774  eqrabdioph  42775  setindtr  43023  gneispace  44133  mnuprdlem3  44273  iunconnlem2  44934  rzalf  45021  fnchoice  45033  refsumcn  45034  rfcnnnub  45040  refsum2cnlem1  45041  iuneq2df  45051  uzwo4  45057  ixpeq2d  45072  ixpssmapc  45077  elintd  45078  ssdf  45079  ralimralim  45085  nelrnmpt  45088  ixpssixp  45096  ballss3  45097  iinssiin  45133  eliind2  45134  rabssd  45146  ss2rabdf  45154  choicefi  45204  iunmapss  45219  iunmapsn  45221  axccdom  45226  mptfnd  45246  ssfiunibd  45318  xralrple2  45361  infxr  45374  xrralrecnnle  45390  xrralrecnnge  45397  supxrunb3  45406  fimaxre4  45408  supxrleubrnmpt  45413  rexabslelem  45425  suprleubrnmpt  45429  uzublem  45437  infxrgelbrnmpt  45461  iooiinicc  45551  iooiinioc  45565  mccl  45607  climsuse  45617  mullimc  45625  mullimcf  45632  limcrecl  45638  limsupre  45650  limcleqr  45653  addlimc  45657  0ellimcdiv  45658  limclner  45660  limsupubuzlem  45721  climinf3  45725  limsupequzmpt2  45727  limsupmnfuzlem  45735  limsupre3uzlem  45744  liminfequzmpt2  45800  cncficcgt0  45897  cncfioobd  45906  fprodsubrecnncnvlem  45916  fprodaddrecnncnvlem  45918  dvmptfprodlem  45953  dvnprodlem1  45955  iblsplitf  45979  stoweidlem5  46014  stoweidlem16  46025  stoweidlem18  46027  stoweidlem21  46030  stoweidlem26  46035  stoweidlem27  46036  stoweidlem28  46037  stoweidlem29  46038  stoweidlem31  46040  stoweidlem34  46043  stoweidlem36  46045  stoweidlem41  46050  stoweidlem42  46051  stoweidlem44  46053  stoweidlem45  46054  stoweidlem48  46057  stoweidlem51  46060  stoweidlem55  46064  stoweidlem59  46068  stoweidlem60  46069  stoweidlem62  46071  wallispilem3  46076  stirlinglem5  46087  fourierdlem16  46132  fourierdlem21  46137  fourierdlem22  46138  fourierdlem31  46147  fourierdlem39  46155  fourierdlem68  46183  fourierdlem71  46186  fourierdlem73  46188  fourierdlem77  46192  fourierdlem80  46195  fourierdlem83  46198  fourierdlem87  46202  fourierdlem94  46209  fourierdlem103  46218  fourierdlem104  46219  fourierdlem112  46227  fourierdlem113  46228  etransclem32  46275  subsaliuncllem  46366  sge0revalmpt  46387  sge0fodjrnlem  46425  sge0fsummptf  46445  iundjiun  46469  meadjiun  46475  voliunsge0lem  46481  meaiininclem  46495  omeiunle  46526  hoicvrrex  46565  ovnsubaddlem2  46580  hoissrrn2  46587  hoidmv1lelem1  46600  hoidmvlelem3  46606  ovnhoilem1  46610  hoi2toco  46616  ovnlecvr2  46619  hspdifhsp  46625  hoiqssbllem1  46631  hoiqssbllem3  46633  hspmbllem2  46636  iinhoiicclem  46682  iunhoiioolem  46684  vonioo  46691  vonicc  46694  pimconstlt0  46710  pimconstlt1  46711  pimltpnff  46712  pimiooltgt  46719  pimdecfgtioc  46724  pimincfltioc  46725  pimdecfgtioo  46726  pimincfltioo  46727  preimageiingt  46729  preimaleiinlt  46730  pimgtmnff  46731  issmfd  46744  issmfdf  46746  sssmf  46747  issmfle  46754  issmfdmpt  46757  issmfgt  46765  issmfled  46766  issmfgtd  46770  smflimlem2  46781  smfmullem4  46803  smfpimcclem  46816  smfsuplem1  46820  smfinflem  46826  iccelpart  47427  mogoldbb  47779  sbgoldbo  47781  pgindnf  49560  aacllem  49645