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 2230	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		ralrimi.2	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	2, 3	hbralrimi 3154	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1812   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1809  df-nf 1813  df-ral 3079

This theorem is used by:  ralrimia  3263  reximdai  3266  r19.37  3267  rexlimd2  3270  r19.12  3313  ralcom2  3365  2rmorex  3716  disjxiun  5105  nelrnmpt  5956  rnmpt0f  6243  fnmptd  6676  mpteqb  7009  fmptdf  7112  eusvobj2  7404  offval2f  7691  zfrep6OLD  7950  frrlem4  8284  tfr3  8384  tz7.49  8430  mapxpen  9129  dfac2b  10121  hsmexlem4  10419  axcc3  10428  domtriomlem  10432  axdc3lem2  10441  axdc3lem4  10443  axdc4lem  10445  ac6num  10469  dedekind  11379  dedekindle  11380  fsuppmapnn0fiublem  14033  fsuppmapnn0fiub  14034  fprodcllemf  16019  lcmfunsnlem1  16701  lcmfunsnlem2lem1  16702  lcmfunsnlem2  16704  mreexexd  17710  cpmatmcllem  22886  ptcnplem  23789  xkocnv  23982  cfilucfil  24727  cncfcompt2  25078  itg2splitlem  25918  itg2split  25919  itgeq1fOLD  25942  bdaypw2n0bndlem  28667  mpteleeOLD  29256  lfgrnloop  29486  foresf1o  32861  iinabrex  32925  funimass4f  32993  fcomptf  33014  aciunf1lem  33018  fnpreimac  33026  prodindf  33193  isarchiofld  33528  reff  34238  locfinreflem  34239  zarclsiin  34270  zarcmplem  34280  esumeq12dvaf  34430  esumgsum  34444  esumel  34446  esumf1o  34449  esumc  34450  esummono  34453  gsumesum  34458  esumlub  34459  esumlef  34461  esumfsup  34469  esumpinfval  34472  esumpinfsum  34476  esum2d  34492  ldsysgenld  34559  sigapildsyslem  34560  ldgenpisyslem1  34562  measinblem  34619  voliune  34628  volmeas  34630  oms0  34696  omssubadd  34699  dstrvprob  34871  bnj1379  35227  bnj1204  35409  bnj1388  35430  bnj1417  35438  bnj1489  35453  untsucf  36210  domalom  38078  fvineqsneq  38086  cover2  38394  upixp  38408  indexdom  38413  filbcmb  38419  sdclem2  38421  eq0rabdioph  43535  eqrabdioph  43536  setindtr  43779  gneispace  44888  mnuprdlem3  45012  iunconnlem2  45671  rzalf  45765  fnchoice  45777  refsumcn  45778  rfcnnnub  45784  refsum2cnlem1  45785  iuneq2df  45795  uzwo4  45801  ixpeq2d  45816  ixpssmapc  45821  elintd  45822  ssdf  45823  ralimralim  45829  ixpssixp  45838  ballss3  45839  iinssiin  45875  eliind2  45876  rabssd  45888  choicefi  45945  iunmapss  45959  iunmapsn  45961  axccdom  45966  mptfnd  45985  ssfiunibd  46056  xralrple2  46098  infxr  46110  xrralrecnnle  46126  xrralrecnnge  46133  supxrunb3  46142  fimaxre4  46143  supxrleubrnmpt  46148  rexabslelem  46160  suprleubrnmpt  46164  uzublem  46172  infxrgelbrnmpt  46196  iooiinicc  46286  iooiinioc  46300  mccl  46342  climsuse  46352  mullimc  46360  mullimcf  46367  limcrecl  46373  limsupre  46383  limcleqr  46386  addlimc  46390  0ellimcdiv  46391  limclner  46393  limsupubuzlem  46454  climinf3  46458  limsupequzmpt2  46460  limsupmnfuzlem  46468  limsupre3uzlem  46477  liminfequzmpt2  46533  cncficcgt0  46630  cncfioobd  46639  fprodsubrecnncnvlem  46649  fprodaddrecnncnvlem  46651  dvmptfprodlem  46686  dvnprodlem1  46688  iblsplitf  46712  stoweidlem5  46747  stoweidlem16  46758  stoweidlem18  46760  stoweidlem21  46763  stoweidlem26  46768  stoweidlem27  46769  stoweidlem28  46770  stoweidlem29  46771  stoweidlem31  46773  stoweidlem34  46776  stoweidlem36  46778  stoweidlem41  46783  stoweidlem42  46784  stoweidlem44  46786  stoweidlem45  46787  stoweidlem48  46790  stoweidlem51  46793  stoweidlem55  46797  stoweidlem59  46801  stoweidlem60  46802  stoweidlem62  46804  wallispilem3  46809  stirlinglem5  46820  fourierdlem16  46865  fourierdlem21  46870  fourierdlem22  46871  fourierdlem31  46880  fourierdlem39  46888  fourierdlem68  46916  fourierdlem71  46919  fourierdlem73  46921  fourierdlem77  46925  fourierdlem80  46928  fourierdlem83  46931  fourierdlem87  46935  fourierdlem94  46942  fourierdlem103  46951  fourierdlem104  46952  fourierdlem112  46960  etransclem32  47008  subsaliuncllem  47099  sge0revalmpt  47120  sge0fodjrnlem  47158  sge0fsummptf  47178  iundjiun  47202  meadjiun  47208  voliunsge0lem  47214  meaiininclem  47228  omeiunle  47259  hoicvrrex  47298  ovnsubaddlem2  47313  hoissrrn2  47320  hoidmv1lelem1  47333  hoidmvlelem3  47339  ovnhoilem1  47343  hoi2toco  47349  ovnlecvr2  47352  hspdifhsp  47358  hoiqssbllem1  47364  hoiqssbllem3  47366  hspmbllem2  47369  iinhoiicclem  47415  iunhoiioolem  47417  vonioo  47424  vonicc  47427  pimconstlt0  47443  pimconstlt1  47444  pimltpnff  47445  pimiooltgt  47452  pimdecfgtioc  47457  pimincfltioc  47458  pimdecfgtioo  47459  pimincfltioo  47460  pimgtmnff  47464  issmfd  47477  issmfdf  47479  issmfle  47487  issmfdmpt  47490  issmfgt  47498  issmfled  47499  issmfgtd  47503  smflimlem2  47514  smfmullem4  47536  smfpimcclem  47549  smfsuplem1  47553  smfinflem  47559  iccelpart  48210  mogoldbb  48578  sbgoldbo  48580  pgindnf  50522  aacllem  50649