Theorem ralrimi 3262

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

Syntax hints:   → wi 4  Ⅎwnf 1805   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-ex 1802  df-nf 1806  df-ral 3079

This theorem is referenced by:  ralrimia  3263  reximdai  3266  r19.37  3267  rexlimd2  3270  r19.12  3313  ralcom2  3366  2rmorex  3719  disjxiun  5099  nelrnmpt  5945  rnmpt0f  6232  fnmptd  6664  mpteqb  6997  fmptdf  7100  eusvobj2  7390  offval2f  7677  zfrep6OLD  7938  frrlem4  8272  tfr3  8372  tz7.49  8418  mapxpen  9117  dfac2b  10089  hsmexlem4  10388  axcc3  10397  domtriomlem  10401  axdc3lem2  10410  axdc3lem4  10412  axdc4lem  10414  ac6num  10438  dedekind  11348  dedekindle  11349  fsuppmapnn0fiublem  14005  fsuppmapnn0fiub  14006  fprodcllemf  15990  lcmfunsnlem1  16673  lcmfunsnlem2lem1  16674  lcmfunsnlem2  16676  mreexexd  17682  cpmatmcllem  22780  ptcnplem  23683  xkocnv  23876  cfilucfil  24621  cncfcompt2  24972  itg2splitlem  25812  itg2split  25813  itgeq1fOLD  25836  bdaypw2n0bndlem  28558  mpteleeOLD  29098  lfgrnloop  29328  foresf1o  32705  iinabrex  32771  funimass4f  32841  fcomptf  32862  aciunf1lem  32866  fnpreimac  32874  prodindf  33042  isarchiofld  33381  reff  34138  locfinreflem  34139  zarclsiin  34170  zarcmplem  34180  esumeq12dvaf  34330  esumgsum  34344  esumel  34346  esumf1o  34349  esumc  34350  esummono  34353  gsumesum  34358  esumlub  34359  esumlef  34361  esumfsup  34369  esumpinfval  34372  esumpinfsum  34376  esum2d  34392  ldsysgenld  34459  sigapildsyslem  34460  ldgenpisyslem1  34462  measinblem  34519  voliune  34528  volmeas  34530  oms0  34596  omssubadd  34599  dstrvprob  34771  bnj1379  35127  bnj1204  35309  bnj1388  35330  bnj1417  35338  bnj1489  35353  untsucf  36065  domalom  37903  fvineqsneq  37911  cover2  38219  upixp  38233  indexdom  38238  filbcmb  38244  sdclem2  38246  eq0rabdioph  43362  eqrabdioph  43363  setindtr  43606  gneispace  44715  mnuprdlem3  44855  iunconnlem2  45515  rzalf  45602  fnchoice  45614  refsumcn  45615  rfcnnnub  45621  refsum2cnlem1  45622  iuneq2df  45632  uzwo4  45638  ixpeq2d  45653  ixpssmapc  45658  elintd  45659  ssdf  45660  ralimralim  45666  ixpssixp  45675  ballss3  45676  iinssiin  45712  eliind2  45713  rabssd  45725  choicefi  45782  iunmapss  45796  iunmapsn  45798  axccdom  45803  mptfnd  45822  ssfiunibd  45893  xralrple2  45935  infxr  45947  xrralrecnnle  45963  xrralrecnnge  45970  supxrunb3  45979  fimaxre4  45980  supxrleubrnmpt  45985  rexabslelem  45997  suprleubrnmpt  46001  uzublem  46009  infxrgelbrnmpt  46033  iooiinicc  46123  iooiinioc  46137  mccl  46179  climsuse  46189  mullimc  46197  mullimcf  46204  limcrecl  46210  limsupre  46220  limcleqr  46223  addlimc  46227  0ellimcdiv  46228  limclner  46230  limsupubuzlem  46291  climinf3  46295  limsupequzmpt2  46297  limsupmnfuzlem  46305  limsupre3uzlem  46314  liminfequzmpt2  46370  cncficcgt0  46467  cncfioobd  46476  fprodsubrecnncnvlem  46486  fprodaddrecnncnvlem  46488  dvmptfprodlem  46523  dvnprodlem1  46525  iblsplitf  46549  stoweidlem5  46584  stoweidlem16  46595  stoweidlem18  46597  stoweidlem21  46600  stoweidlem26  46605  stoweidlem27  46606  stoweidlem28  46607  stoweidlem29  46608  stoweidlem31  46610  stoweidlem34  46613  stoweidlem36  46615  stoweidlem41  46620  stoweidlem42  46621  stoweidlem44  46623  stoweidlem45  46624  stoweidlem48  46627  stoweidlem51  46630  stoweidlem55  46634  stoweidlem59  46638  stoweidlem60  46639  stoweidlem62  46641  wallispilem3  46646  stirlinglem5  46657  fourierdlem16  46702  fourierdlem21  46707  fourierdlem22  46708  fourierdlem31  46717  fourierdlem39  46725  fourierdlem68  46753  fourierdlem71  46756  fourierdlem73  46758  fourierdlem77  46762  fourierdlem80  46765  fourierdlem83  46768  fourierdlem87  46772  fourierdlem94  46779  fourierdlem103  46788  fourierdlem104  46789  fourierdlem112  46797  etransclem32  46845  subsaliuncllem  46936  sge0revalmpt  46957  sge0fodjrnlem  46995  sge0fsummptf  47015  iundjiun  47039  meadjiun  47045  voliunsge0lem  47051  meaiininclem  47065  omeiunle  47096  hoicvrrex  47135  ovnsubaddlem2  47150  hoissrrn2  47157  hoidmv1lelem1  47170  hoidmvlelem3  47176  ovnhoilem1  47180  hoi2toco  47186  ovnlecvr2  47189  hspdifhsp  47195  hoiqssbllem1  47201  hoiqssbllem3  47203  hspmbllem2  47206  iinhoiicclem  47252  iunhoiioolem  47254  vonioo  47261  vonicc  47264  pimconstlt0  47280  pimconstlt1  47281  pimltpnff  47282  pimiooltgt  47289  pimdecfgtioc  47294  pimincfltioc  47295  pimdecfgtioo  47296  pimincfltioo  47297  pimgtmnff  47301  issmfd  47314  issmfdf  47316  issmfle  47324  issmfdmpt  47327  issmfgt  47335  issmfled  47336  issmfgtd  47340  smflimlem2  47351  smfmullem4  47373  smfpimcclem  47386  smfsuplem1  47390  smfinflem  47396  iccelpart  48044  mogoldbb  48412  sbgoldbo  48414  pgindnf  50342  aacllem  50427