Theorem ralrimi 3233

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

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

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 2183

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

This theorem is referenced by:  ralrimia  3234  ralimdaa  3236  reximdai  3237  r19.37  3238  rexlimd2  3241  r19.12  3284  ralcom2  3346  rabbidaOLD  3436  2rmorex  3711  iineq2d  4969  disjxiun  5094  nelrnmpt  5915  rnmpt0f  6200  fnmptd  6632  mpteqb  6960  fmptdf  7062  eusvobj2  7350  offval2f  7637  zfrep6  7899  frrlem4  8231  tfr3  8330  tz7.49  8376  mapxpen  9073  dfac2b  10043  hsmexlem4  10341  axcc3  10350  domtriomlem  10354  axdc3lem2  10363  axdc3lem4  10365  axdc4lem  10367  ac6num  10391  dedekind  11298  dedekindle  11299  fsuppmapnn0fiublem  13915  fsuppmapnn0fiub  13916  fprodcllemf  15883  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem2  16569  mreexexd  17573  cpmatmcllem  22664  ptcnplem  23567  xkocnv  23760  cfilucfil  24505  cncfcompt2  24859  itg2splitlem  25707  itg2split  25708  itgeq1fOLD  25731  bdaypw2n0sbndlem  28440  mpteleeOLD  28949  lfgrnloop  29179  foresf1o  32559  iinabrex  32624  funimass4f  32695  fcomptf  32716  aciunf1lem  32720  fnpreimac  32728  prodindf  32923  isarchiofld  33260  reff  33975  locfinreflem  33976  zarclsiin  34007  zarcmplem  34017  esumeq12dvaf  34167  esumgsum  34181  esumel  34183  esumf1o  34186  esumc  34187  esummono  34190  gsumesum  34195  esumlub  34196  esumlef  34198  esumfsup  34206  esumpinfval  34209  esumpinfsum  34213  esum2d  34229  ldsysgenld  34296  sigapildsyslem  34297  ldgenpisyslem1  34299  measinblem  34356  voliune  34365  volmeas  34367  oms0  34433  omssubadd  34436  dstrvprob  34608  bnj1379  34965  bnj1204  35147  bnj1388  35168  bnj1417  35176  bnj1489  35191  untsucf  35883  domalom  37578  fvineqsneq  37586  cover2  37885  upixp  37899  indexdom  37904  filbcmb  37910  sdclem2  37912  eq0rabdioph  43055  eqrabdioph  43056  setindtr  43303  gneispace  44412  mnuprdlem3  44552  iunconnlem2  45212  rzalf  45299  fnchoice  45311  refsumcn  45312  rfcnnnub  45318  refsum2cnlem1  45319  iuneq2df  45329  uzwo4  45335  ixpeq2d  45350  ixpssmapc  45355  elintd  45356  ssdf  45357  ralimralim  45363  ixpssixp  45373  ballss3  45374  iinssiin  45410  eliind2  45411  rabssd  45423  choicefi  45481  iunmapss  45496  iunmapsn  45498  axccdom  45503  mptfnd  45523  ssfiunibd  45594  xralrple2  45636  infxr  45648  xrralrecnnle  45664  xrralrecnnge  45671  supxrunb3  45680  fimaxre4  45682  supxrleubrnmpt  45687  rexabslelem  45699  suprleubrnmpt  45703  uzublem  45711  infxrgelbrnmpt  45735  iooiinicc  45825  iooiinioc  45839  mccl  45881  climsuse  45891  mullimc  45899  mullimcf  45906  limcrecl  45912  limsupre  45922  limcleqr  45925  addlimc  45929  0ellimcdiv  45930  limclner  45932  limsupubuzlem  45993  climinf3  45997  limsupequzmpt2  45999  limsupmnfuzlem  46007  limsupre3uzlem  46016  liminfequzmpt2  46072  cncficcgt0  46169  cncfioobd  46178  fprodsubrecnncnvlem  46188  fprodaddrecnncnvlem  46190  dvmptfprodlem  46225  dvnprodlem1  46227  iblsplitf  46251  stoweidlem5  46286  stoweidlem16  46297  stoweidlem18  46299  stoweidlem21  46302  stoweidlem26  46307  stoweidlem27  46308  stoweidlem28  46309  stoweidlem29  46310  stoweidlem31  46312  stoweidlem34  46315  stoweidlem36  46317  stoweidlem41  46322  stoweidlem42  46323  stoweidlem44  46325  stoweidlem45  46326  stoweidlem48  46329  stoweidlem51  46332  stoweidlem55  46336  stoweidlem59  46340  stoweidlem60  46341  stoweidlem62  46343  wallispilem3  46348  stirlinglem5  46359  fourierdlem16  46404  fourierdlem21  46409  fourierdlem22  46410  fourierdlem31  46419  fourierdlem39  46427  fourierdlem68  46455  fourierdlem71  46458  fourierdlem73  46460  fourierdlem77  46464  fourierdlem80  46467  fourierdlem83  46470  fourierdlem87  46474  fourierdlem94  46481  fourierdlem103  46490  fourierdlem104  46491  fourierdlem112  46499  fourierdlem113  46500  etransclem32  46547  subsaliuncllem  46638  sge0revalmpt  46659  sge0fodjrnlem  46697  sge0fsummptf  46717  iundjiun  46741  meadjiun  46747  voliunsge0lem  46753  meaiininclem  46767  omeiunle  46798  hoicvrrex  46837  ovnsubaddlem2  46852  hoissrrn2  46859  hoidmv1lelem1  46872  hoidmvlelem3  46878  ovnhoilem1  46882  hoi2toco  46888  ovnlecvr2  46891  hspdifhsp  46897  hoiqssbllem1  46903  hoiqssbllem3  46905  hspmbllem2  46908  iinhoiicclem  46954  iunhoiioolem  46956  vonioo  46963  vonicc  46966  pimconstlt0  46982  pimconstlt1  46983  pimltpnff  46984  pimiooltgt  46991  pimdecfgtioc  46996  pimincfltioc  46997  pimdecfgtioo  46998  pimincfltioo  46999  pimgtmnff  47003  issmfd  47016  issmfdf  47018  sssmf  47019  issmfle  47026  issmfdmpt  47029  issmfgt  47037  issmfled  47038  issmfgtd  47042  smflimlem2  47053  smfmullem4  47075  smfpimcclem  47088  smfsuplem1  47092  smfinflem  47098  iccelpart  47716  mogoldbb  48068  sbgoldbo  48070  pgindnf  49998  aacllem  50083