Theorem ralrimi 3236

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

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

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 3053

This theorem is referenced by:  ralrimia  3237  ralimdaa  3239  reximdai  3240  r19.37  3241  rexlimd2  3244  r19.12  3287  ralcom2  3349  rabbidaOLD  3439  2rmorex  3714  iineq2d  4972  disjxiun  5097  nelrnmpt  5926  rnmpt0f  6211  fnmptd  6643  mpteqb  6971  fmptdf  7073  eusvobj2  7362  offval2f  7649  zfrep6OLD  7911  frrlem4  8243  tfr3  8342  tz7.49  8388  mapxpen  9085  dfac2b  10055  hsmexlem4  10353  axcc3  10362  domtriomlem  10366  axdc3lem2  10375  axdc3lem4  10377  axdc4lem  10379  ac6num  10403  dedekind  11310  dedekindle  11311  fsuppmapnn0fiublem  13927  fsuppmapnn0fiub  13928  fprodcllemf  15895  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmfunsnlem2  16581  mreexexd  17585  cpmatmcllem  22679  ptcnplem  23582  xkocnv  23775  cfilucfil  24520  cncfcompt2  24874  itg2splitlem  25722  itg2split  25723  itgeq1fOLD  25746  bdaypw2n0bndlem  28476  mpteleeOLD  28986  lfgrnloop  29216  foresf1o  32597  iinabrex  32662  funimass4f  32733  fcomptf  32754  aciunf1lem  32758  fnpreimac  32766  prodindf  32961  isarchiofld  33299  reff  34023  locfinreflem  34024  zarclsiin  34055  zarcmplem  34065  esumeq12dvaf  34215  esumgsum  34229  esumel  34231  esumf1o  34234  esumc  34235  esummono  34238  gsumesum  34243  esumlub  34244  esumlef  34246  esumfsup  34254  esumpinfval  34257  esumpinfsum  34261  esum2d  34277  ldsysgenld  34344  sigapildsyslem  34345  ldgenpisyslem1  34347  measinblem  34404  voliune  34413  volmeas  34415  oms0  34481  omssubadd  34484  dstrvprob  34656  bnj1379  35012  bnj1204  35194  bnj1388  35215  bnj1417  35223  bnj1489  35238  untsucf  35932  domalom  37686  fvineqsneq  37694  cover2  37995  upixp  38009  indexdom  38014  filbcmb  38020  sdclem2  38022  eq0rabdioph  43162  eqrabdioph  43163  setindtr  43410  gneispace  44519  mnuprdlem3  44659  iunconnlem2  45319  rzalf  45406  fnchoice  45418  refsumcn  45419  rfcnnnub  45425  refsum2cnlem1  45426  iuneq2df  45436  uzwo4  45442  ixpeq2d  45457  ixpssmapc  45462  elintd  45463  ssdf  45464  ralimralim  45470  ixpssixp  45480  ballss3  45481  iinssiin  45517  eliind2  45518  rabssd  45530  choicefi  45587  iunmapss  45602  iunmapsn  45604  axccdom  45609  mptfnd  45629  ssfiunibd  45700  xralrple2  45742  infxr  45754  xrralrecnnle  45770  xrralrecnnge  45777  supxrunb3  45786  fimaxre4  45788  supxrleubrnmpt  45793  rexabslelem  45805  suprleubrnmpt  45809  uzublem  45817  infxrgelbrnmpt  45841  iooiinicc  45931  iooiinioc  45945  mccl  45987  climsuse  45997  mullimc  46005  mullimcf  46012  limcrecl  46018  limsupre  46028  limcleqr  46031  addlimc  46035  0ellimcdiv  46036  limclner  46038  limsupubuzlem  46099  climinf3  46103  limsupequzmpt2  46105  limsupmnfuzlem  46113  limsupre3uzlem  46122  liminfequzmpt2  46178  cncficcgt0  46275  cncfioobd  46284  fprodsubrecnncnvlem  46294  fprodaddrecnncnvlem  46296  dvmptfprodlem  46331  dvnprodlem1  46333  iblsplitf  46357  stoweidlem5  46392  stoweidlem16  46403  stoweidlem18  46405  stoweidlem21  46408  stoweidlem26  46413  stoweidlem27  46414  stoweidlem28  46415  stoweidlem29  46416  stoweidlem31  46418  stoweidlem34  46421  stoweidlem36  46423  stoweidlem41  46428  stoweidlem42  46429  stoweidlem44  46431  stoweidlem45  46432  stoweidlem48  46435  stoweidlem51  46438  stoweidlem55  46442  stoweidlem59  46446  stoweidlem60  46447  stoweidlem62  46449  wallispilem3  46454  stirlinglem5  46465  fourierdlem16  46510  fourierdlem21  46515  fourierdlem22  46516  fourierdlem31  46525  fourierdlem39  46533  fourierdlem68  46561  fourierdlem71  46564  fourierdlem73  46566  fourierdlem77  46570  fourierdlem80  46573  fourierdlem83  46576  fourierdlem87  46580  fourierdlem94  46587  fourierdlem103  46596  fourierdlem104  46597  fourierdlem112  46605  fourierdlem113  46606  etransclem32  46653  subsaliuncllem  46744  sge0revalmpt  46765  sge0fodjrnlem  46803  sge0fsummptf  46823  iundjiun  46847  meadjiun  46853  voliunsge0lem  46859  meaiininclem  46873  omeiunle  46904  hoicvrrex  46943  ovnsubaddlem2  46958  hoissrrn2  46965  hoidmv1lelem1  46978  hoidmvlelem3  46984  ovnhoilem1  46988  hoi2toco  46994  ovnlecvr2  46997  hspdifhsp  47003  hoiqssbllem1  47009  hoiqssbllem3  47011  hspmbllem2  47014  iinhoiicclem  47060  iunhoiioolem  47062  vonioo  47069  vonicc  47072  pimconstlt0  47088  pimconstlt1  47089  pimltpnff  47090  pimiooltgt  47097  pimdecfgtioc  47102  pimincfltioc  47103  pimdecfgtioo  47104  pimincfltioo  47105  pimgtmnff  47109  issmfd  47122  issmfdf  47124  sssmf  47125  issmfle  47132  issmfdmpt  47135  issmfgt  47143  issmfled  47144  issmfgtd  47148  smflimlem2  47159  smfmullem4  47181  smfpimcclem  47194  smfsuplem1  47198  smfinflem  47204  iccelpart  47822  mogoldbb  48174  sbgoldbo  48176  pgindnf  50104  aacllem  50189