Theorem ralrimi 3256

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

Syntax hints:   → wi 4  Ⅎwnf 1782   ∈ wcel 2107  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783  df-ral 3061

This theorem is referenced by:  ralrimia  3257  ralimdaa  3259  reximdai  3260  r19.37  3261  rexlimd2  3264  r19.12  3313  r19.12OLD  3314  ralcom2  3376  rabbidaOLD  3476  2rmorex  3759  iineq2d  5014  disjxiun  5139  mpteq2daOLD  5240  rnmpt0f  6262  fnmptd  6708  mpteqb  7034  fmptdf  7136  eusvobj2  7424  offval2f  7713  zfrep6  7980  frrlem4  8315  wfrlem4OLD  8353  tfr3  8440  tz7.49  8486  mapxpen  9184  dfac2b  10172  hsmexlem4  10470  axcc3  10479  domtriomlem  10483  axdc3lem2  10492  axdc3lem4  10494  axdc4lem  10496  ac6num  10520  dedekind  11425  dedekindle  11426  fsuppmapnn0fiublem  14032  fsuppmapnn0fiub  14033  fprodcllemf  15995  lcmfunsnlem1  16675  lcmfunsnlem2lem1  16676  lcmfunsnlem2  16678  mreexexd  17692  cpmatmcllem  22725  ptcnplem  23630  xkocnv  23823  cfilucfil  24573  cncfcompt2  24935  itg2splitlem  25784  itg2split  25785  itgeq1fOLD  25808  mptelee  28911  lfgrnloop  29143  foresf1o  32524  iinabrex  32583  funimass4f  32648  fcomptf  32669  aciunf1lem  32673  funcnvmpt  32678  fnpreimac  32682  prodindf  32849  isarchiofld  33348  reff  33839  locfinreflem  33840  zarclsiin  33871  zarcmplem  33881  esumeq12dvaf  34033  esumgsum  34047  esumel  34049  esumf1o  34052  esumc  34053  esummono  34056  gsumesum  34061  esumlub  34062  esumlef  34064  esumfsup  34072  esumpinfval  34075  esumpinfsum  34079  esum2d  34095  ldsysgenld  34162  sigapildsyslem  34163  ldgenpisyslem1  34165  measinblem  34222  voliune  34231  volmeas  34233  oms0  34300  omssubadd  34303  dstrvprob  34475  bnj1379  34845  bnj1204  35027  bnj1388  35048  bnj1417  35056  bnj1489  35071  untsucf  35711  domalom  37406  fvineqsneq  37414  cover2  37723  upixp  37737  indexdom  37742  filbcmb  37748  sdclem2  37750  eq0rabdioph  42792  eqrabdioph  42793  setindtr  43041  gneispace  44152  mnuprdlem3  44298  iunconnlem2  44960  rzalf  45027  fnchoice  45039  refsumcn  45040  rfcnnnub  45046  refsum2cnlem1  45047  iuneq2df  45057  uzwo4  45063  ixpeq2d  45078  ixpssmapc  45083  elintd  45084  ssdf  45085  ralimralim  45091  nelrnmpt  45094  ixpssixp  45102  ballss3  45103  iinssiin  45139  eliind2  45140  rabssd  45152  ss2rabdf  45160  choicefi  45210  iunmapss  45225  iunmapsn  45227  axccdom  45232  mptfnd  45253  ssfiunibd  45326  xralrple2  45370  infxr  45383  xrralrecnnle  45399  xrralrecnnge  45406  supxrunb3  45415  fimaxre4  45417  supxrleubrnmpt  45422  rexabslelem  45434  suprleubrnmpt  45438  uzublem  45446  infxrgelbrnmpt  45470  iooiinicc  45560  iooiinioc  45574  mccl  45618  climsuse  45628  mullimc  45636  mullimcf  45643  limcrecl  45649  limsupre  45661  limcleqr  45664  addlimc  45668  0ellimcdiv  45669  limclner  45671  limsupubuzlem  45732  climinf3  45736  limsupequzmpt2  45738  limsupmnfuzlem  45746  limsupre3uzlem  45755  liminfequzmpt2  45811  cncficcgt0  45908  cncfioobd  45917  fprodsubrecnncnvlem  45927  fprodaddrecnncnvlem  45929  dvmptfprodlem  45964  dvnprodlem1  45966  iblsplitf  45990  stoweidlem5  46025  stoweidlem16  46036  stoweidlem18  46038  stoweidlem21  46041  stoweidlem26  46046  stoweidlem27  46047  stoweidlem28  46048  stoweidlem29  46049  stoweidlem31  46051  stoweidlem34  46054  stoweidlem36  46056  stoweidlem41  46061  stoweidlem42  46062  stoweidlem44  46064  stoweidlem45  46065  stoweidlem48  46068  stoweidlem51  46071  stoweidlem55  46075  stoweidlem59  46079  stoweidlem60  46080  stoweidlem62  46082  wallispilem3  46087  stirlinglem5  46098  fourierdlem16  46143  fourierdlem21  46148  fourierdlem22  46149  fourierdlem31  46158  fourierdlem39  46166  fourierdlem68  46194  fourierdlem71  46197  fourierdlem73  46199  fourierdlem77  46203  fourierdlem80  46206  fourierdlem83  46209  fourierdlem87  46213  fourierdlem94  46220  fourierdlem103  46229  fourierdlem104  46230  fourierdlem112  46238  fourierdlem113  46239  etransclem32  46286  subsaliuncllem  46377  sge0revalmpt  46398  sge0fodjrnlem  46436  sge0fsummptf  46456  iundjiun  46480  meadjiun  46486  voliunsge0lem  46492  meaiininclem  46506  omeiunle  46537  hoicvrrex  46576  ovnsubaddlem2  46591  hoissrrn2  46598  hoidmv1lelem1  46611  hoidmvlelem3  46617  ovnhoilem1  46621  hoi2toco  46627  ovnlecvr2  46630  hspdifhsp  46636  hoiqssbllem1  46642  hoiqssbllem3  46644  hspmbllem2  46647  iinhoiicclem  46693  iunhoiioolem  46695  vonioo  46702  vonicc  46705  pimconstlt0  46721  pimconstlt1  46722  pimltpnff  46723  pimiooltgt  46730  pimdecfgtioc  46735  pimincfltioc  46736  pimdecfgtioo  46737  pimincfltioo  46738  preimageiingt  46740  preimaleiinlt  46741  pimgtmnff  46742  issmfd  46755  issmfdf  46757  sssmf  46758  issmfle  46765  issmfdmpt  46768  issmfgt  46776  issmfled  46777  issmfgtd  46781  smflimlem2  46792  smfmullem4  46814  smfpimcclem  46827  smfsuplem1  46831  smfinflem  46837  iccelpart  47425  mogoldbb  47777  sbgoldbo  47779  pgindnf  49290  aacllem  49375