Theorem ralrimi 3235

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). For a version based on fewer axioms see ralrimiv 3128. (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3127. (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 2203	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		ralrimi.2	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	2, 3	hbralrimi 3127	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786  df-ral 3052

This theorem is referenced by:  ralrimia  3236  reximdai  3239  r19.37  3240  rexlimd2  3243  r19.12  3286  ralcom2  3339  2rmorex  3700  disjxiun  5082  nelrnmpt  5922  rnmpt0f  6207  fnmptd  6639  mpteqb  6967  fmptdf  7069  eusvobj2  7359  offval2f  7646  zfrep6OLD  7908  frrlem4  8239  tfr3  8338  tz7.49  8384  mapxpen  9081  dfac2b  10053  hsmexlem4  10351  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  ac6num  10401  dedekind  11309  dedekindle  11310  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  fprodcllemf  15923  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  mreexexd  17614  cpmatmcllem  22683  ptcnplem  23586  xkocnv  23779  cfilucfil  24524  cncfcompt2  24875  itg2splitlem  25715  itg2split  25716  itgeq1fOLD  25739  bdaypw2n0bndlem  28455  mpteleeOLD  28964  lfgrnloop  29194  foresf1o  32574  iinabrex  32639  funimass4f  32710  fcomptf  32731  aciunf1lem  32735  fnpreimac  32743  prodindf  32922  isarchiofld  33260  reff  33983  locfinreflem  33984  zarclsiin  34015  zarcmplem  34025  esumeq12dvaf  34175  esumgsum  34189  esumel  34191  esumf1o  34194  esumc  34195  esummono  34198  gsumesum  34203  esumlub  34204  esumlef  34206  esumfsup  34214  esumpinfval  34217  esumpinfsum  34221  esum2d  34237  ldsysgenld  34304  sigapildsyslem  34305  ldgenpisyslem1  34307  measinblem  34364  voliune  34373  volmeas  34375  oms0  34441  omssubadd  34444  dstrvprob  34616  bnj1379  34972  bnj1204  35154  bnj1388  35175  bnj1417  35183  bnj1489  35198  untsucf  35892  domalom  37720  fvineqsneq  37728  cover2  38036  upixp  38050  indexdom  38055  filbcmb  38061  sdclem2  38063  eq0rabdioph  43208  eqrabdioph  43209  setindtr  43452  gneispace  44561  mnuprdlem3  44701  iunconnlem2  45361  rzalf  45448  fnchoice  45460  refsumcn  45461  rfcnnnub  45467  refsum2cnlem1  45468  iuneq2df  45478  uzwo4  45484  ixpeq2d  45499  ixpssmapc  45504  elintd  45505  ssdf  45506  ralimralim  45512  ixpssixp  45522  ballss3  45523  iinssiin  45559  eliind2  45560  rabssd  45572  choicefi  45629  iunmapss  45644  iunmapsn  45646  axccdom  45651  mptfnd  45671  ssfiunibd  45742  xralrple2  45784  infxr  45796  xrralrecnnle  45812  xrralrecnnge  45819  supxrunb3  45828  fimaxre4  45829  supxrleubrnmpt  45834  rexabslelem  45846  suprleubrnmpt  45850  uzublem  45858  infxrgelbrnmpt  45882  iooiinicc  45972  iooiinioc  45986  mccl  46028  climsuse  46038  mullimc  46046  mullimcf  46053  limcrecl  46059  limsupre  46069  limcleqr  46072  addlimc  46076  0ellimcdiv  46077  limclner  46079  limsupubuzlem  46140  climinf3  46144  limsupequzmpt2  46146  limsupmnfuzlem  46154  limsupre3uzlem  46163  liminfequzmpt2  46219  cncficcgt0  46316  cncfioobd  46325  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  dvmptfprodlem  46372  dvnprodlem1  46374  iblsplitf  46398  stoweidlem5  46433  stoweidlem16  46444  stoweidlem18  46446  stoweidlem21  46449  stoweidlem26  46454  stoweidlem27  46455  stoweidlem28  46456  stoweidlem29  46457  stoweidlem31  46459  stoweidlem34  46462  stoweidlem36  46464  stoweidlem41  46469  stoweidlem42  46470  stoweidlem44  46472  stoweidlem45  46473  stoweidlem48  46476  stoweidlem51  46479  stoweidlem55  46483  stoweidlem59  46487  stoweidlem60  46488  stoweidlem62  46490  wallispilem3  46495  stirlinglem5  46506  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem31  46566  fourierdlem39  46574  fourierdlem68  46602  fourierdlem71  46605  fourierdlem73  46607  fourierdlem77  46611  fourierdlem80  46614  fourierdlem83  46617  fourierdlem87  46621  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  etransclem32  46694  subsaliuncllem  46785  sge0revalmpt  46806  sge0fodjrnlem  46844  sge0fsummptf  46864  iundjiun  46888  meadjiun  46894  voliunsge0lem  46900  meaiininclem  46914  omeiunle  46945  hoicvrrex  46984  ovnsubaddlem2  46999  hoissrrn2  47006  hoidmv1lelem1  47019  hoidmvlelem3  47025  ovnhoilem1  47029  hoi2toco  47035  ovnlecvr2  47038  hspdifhsp  47044  hoiqssbllem1  47050  hoiqssbllem3  47052  hspmbllem2  47055  iinhoiicclem  47101  iunhoiioolem  47103  vonioo  47110  vonicc  47113  pimconstlt0  47129  pimconstlt1  47130  pimltpnff  47131  pimiooltgt  47138  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  pimgtmnff  47150  issmfd  47163  issmfdf  47165  sssmf  47166  issmfle  47173  issmfdmpt  47176  issmfgt  47184  issmfled  47185  issmfgtd  47189  smflimlem2  47200  smfmullem4  47222  smfpimcclem  47235  smfsuplem1  47239  smfinflem  47245  iccelpart  47893  mogoldbb  48261  sbgoldbo  48263  pgindnf  50191  aacllem  50276