Theorem ralrimi 3260

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816  df-ral 3077

This theorem is used by:  ralrimia  3261  reximdai  3264  r19.37  3265  rexlimd2  3268  r19.12  3311  ralcom2  3362  2rmorex  3711  disjxiun  5099  nelrnmpt  5948  rnmpt0f  6244  fnmptd  6680  mpteqb  7013  fmptdf  7117  eusvobj2  7412  offval2f  7708  zfrep6OLD  7967  frrlem4  8307  tfr3  8407  tz7.49  8455  mapxpen  9162  dfac2b  10209  hsmexlem4  10507  axcc3  10516  domtriomlem  10520  axdc3lem2  10529  axdc3lem4  10531  axdc4lem  10533  ac6num  10557  dedekind  11473  dedekindle  11474  fsuppmapnn0fiublem  14133  fsuppmapnn0fiub  14134  fprodcllemf  16125  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem2  16815  mreexexd  17822  cpmatmcllem  23036  ptcnplem  23940  xkocnv  24133  cfilucfil  24878  cncfcompt2  25229  itg2splitlem  26069  itg2split  26070  bdaypw2n0bndlem  28849  mpteleeOLD  29473  lfgrnloop  29703  foresf1o  33142  iinabrex  33205  funimass4f  33273  fcomptf  33294  aciunf1lem  33298  fnpreimac  33306  prodindf  33471  isarchiofld  33802  reff  34513  locfinreflem  34514  zarclsiin  34545  zarcmplem  34555  esumeq12dvaf  34705  esumgsum  34719  esumel  34721  esumf1o  34724  esumc  34725  esummono  34728  gsumesum  34733  esumlub  34734  esumlef  34736  esumfsup  34744  esumpinfval  34747  esumpinfsum  34751  esum2d  34767  ldsysgenld  34835  sigapildsyslem  34836  ldgenpisyslem1  34838  measinblem  34895  voliune  34904  volmeas  34906  oms0  34971  omssubadd  34974  dstrvprob  35146  bnj1379  35502  bnj1204  35684  bnj1388  35705  bnj1417  35713  bnj1489  35728  untsucf  36517  domalom  38370  fvineqsneq  38378  cover2  38692  upixp  38706  indexdom  38711  filbcmb  38717  sdclem2  38719  eq0rabdioph  43830  eqrabdioph  43831  setindtr  44074  gneispace  45177  mnuprdlem3  45301  iunconnlem2  45960  rzalf  46077  fnchoice  46089  refsumcn  46090  rfcnnnub  46096  refsum2cnlem1  46097  iuneq2df  46107  uzwo4  46113  ixpeq2d  46128  ixpssmapc  46133  elintd  46134  ssdf  46135  ralimralim  46141  ixpssixp  46150  ballss3  46151  iinssiin  46187  eliind2  46188  rabssd  46200  choicefi  46257  iunmapss  46271  iunmapsn  46273  axccdom  46278  mptfnd  46297  ssfiunibd  46368  xralrple2  46409  infxr  46421  xrralrecnnle  46437  xrralrecnnge  46444  supxrunb3  46453  fimaxre4  46454  supxrleubrnmpt  46459  rexabslelem  46471  suprleubrnmpt  46475  uzublem  46483  infxrgelbrnmpt  46507  iooiinicc  46597  iooiinioc  46611  mccl  46653  climsuse  46663  mullimc  46671  mullimcf  46678  limcrecl  46684  limsupre  46694  limcleqr  46697  addlimc  46701  0ellimcdiv  46702  limclner  46704  limsupubuzlem  46765  climinf3  46769  limsupequzmpt2  46771  limsupmnfuzlem  46779  limsupre3uzlem  46788  liminfequzmpt2  46844  cncficcgt0  46941  cncfioobd  46950  fprodsubrecnncnvlem  46960  fprodaddrecnncnvlem  46962  dvmptfprodlem  46997  dvnprodlem1  46999  iblsplitf  47023  stoweidlem5  47058  stoweidlem16  47069  stoweidlem18  47071  stoweidlem21  47074  stoweidlem26  47079  stoweidlem27  47080  stoweidlem28  47081  stoweidlem29  47082  stoweidlem31  47084  stoweidlem34  47087  stoweidlem36  47089  stoweidlem41  47094  stoweidlem42  47095  stoweidlem44  47097  stoweidlem45  47098  stoweidlem48  47101  stoweidlem51  47104  stoweidlem55  47108  stoweidlem59  47112  stoweidlem60  47113  stoweidlem62  47115  wallispilem3  47120  stirlinglem5  47131  fourierdlem16  47176  fourierdlem21  47181  fourierdlem22  47182  fourierdlem31  47191  fourierdlem39  47199  fourierdlem68  47227  fourierdlem71  47230  fourierdlem73  47232  fourierdlem77  47236  fourierdlem80  47239  fourierdlem83  47242  fourierdlem87  47246  fourierdlem94  47253  fourierdlem103  47262  fourierdlem104  47263  fourierdlem112  47271  etransclem32  47319  subsaliuncllem  47410  sge0revalmpt  47431  sge0fodjrnlem  47469  sge0fsummptf  47489  iundjiun  47513  meadjiun  47519  voliunsge0lem  47525  meaiininclem  47539  omeiunle  47570  hoicvrrex  47609  ovnsubaddlem2  47624  hoissrrn2  47631  hoidmv1lelem1  47644  hoidmvlelem3  47650  ovnhoilem1  47654  hoi2toco  47660  ovnlecvr2  47663  hspdifhsp  47669  hoiqssbllem1  47675  hoiqssbllem3  47677  hspmbllem2  47680  iinhoiicclem  47726  iunhoiioolem  47728  vonioo  47735  vonicc  47738  pimconstlt0  47754  pimconstlt1  47755  pimltpnff  47756  pimiooltgt  47763  pimdecfgtioc  47768  pimincfltioc  47769  pimdecfgtioo  47770  pimincfltioo  47771  pimgtmnff  47775  issmfd  47788  issmfdf  47790  issmfle  47798  issmfdmpt  47801  issmfgt  47809  issmfled  47810  issmfgtd  47814  smflimlem2  47825  smfmullem4  47847  smfpimcclem  47860  smfsuplem1  47864  smfinflem  47870  iccelpart  48558  mogoldbb  48926  sbgoldbo  48928  pgindnf  50852  aacllem  50982