Theorem ralrimi 3255

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

Syntax hints:   → wi 4  Ⅎwnf 1786   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-ral 3063

This theorem is referenced by:  ralrimia  3256  ralimdaa  3258  reximdai  3259  r19.37  3260  rexlimd2  3263  r19.12  3312  r19.12OLD  3313  ralcom2  3374  rabbidaOLD  3471  2rmorex  3751  iineq2d  5021  disjxiun  5146  mpteq2daOLD  5248  rnmpt0f  6243  fnmptd  6692  mpteqb  7018  fmptdf  7117  eusvobj2  7401  offval2f  7685  zfrep6  7941  frrlem4  8274  wfrlem4OLD  8312  tfr3  8399  tz7.49  8445  mapxpen  9143  dfac2b  10125  hsmexlem4  10424  axcc3  10433  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  ac6num  10474  dedekind  11377  dedekindle  11378  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fprodcllemf  15902  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmfunsnlem2  16577  mreexexd  17592  cpmatmcllem  22220  ptcnplem  23125  xkocnv  23318  cfilucfil  24068  cncfcompt2  24424  itg2splitlem  25266  itg2split  25267  itgeq1f  25289  mptelee  28184  lfgrnloop  28416  foresf1o  31773  iinabrex  31831  funimass4f  31892  fcomptf  31914  aciunf1lem  31918  funcnvmpt  31923  fnpreimac  31927  isarchiofld  32466  reff  32850  locfinreflem  32851  zarclsiin  32882  zarcmplem  32892  prodindf  33052  esumeq12dvaf  33060  esumgsum  33074  esumel  33076  esumf1o  33079  esumc  33080  esummono  33083  gsumesum  33088  esumlub  33089  esumlef  33091  esumfsup  33099  esumpinfval  33102  esumpinfsum  33106  esum2d  33122  ldsysgenld  33189  sigapildsyslem  33190  ldgenpisyslem1  33192  measinblem  33249  voliune  33258  volmeas  33260  oms0  33327  omssubadd  33330  dstrvprob  33501  bnj1379  33872  bnj1204  34054  bnj1388  34075  bnj1417  34083  bnj1489  34098  untsucf  34710  domalom  36333  fvineqsneq  36341  cover2  36631  upixp  36645  indexdom  36650  filbcmb  36656  sdclem2  36658  eq0rabdioph  41562  eqrabdioph  41563  setindtr  41811  gneispace  42933  mnuprdlem3  43081  iunconnlem2  43744  rzalf  43749  fnchoice  43761  refsumcn  43762  rfcnnnub  43768  refsum2cnlem1  43769  iuneq2df  43781  uzwo4  43788  ixpeq2d  43803  ixpssmapc  43809  elintd  43811  ssdf  43812  ralimralim  43818  nelrnmpt  43821  ixpssixp  43829  ballss3  43830  iinssiin  43866  eliind2  43867  rabssd  43879  ss2rabdf  43892  fompt  43938  choicefi  43947  iunmapss  43962  iunmapsn  43964  axccdom  43969  mptfnd  43993  ssfiunibd  44067  xralrple2  44112  infxr  44125  xrralrecnnle  44141  xrralrecnnge  44148  supxrunb3  44157  fimaxre4  44159  supxrleubrnmpt  44164  rexabslelem  44176  suprleubrnmpt  44180  uzublem  44188  infxrgelbrnmpt  44212  iooiinicc  44303  iooiinioc  44317  mccl  44362  climsuse  44372  mullimc  44380  mullimcf  44387  limcrecl  44393  limsupre  44405  limcleqr  44408  addlimc  44412  0ellimcdiv  44413  limclner  44415  limsupubuzlem  44476  climinf3  44480  limsupequzmpt2  44482  limsupmnfuzlem  44490  limsupre3uzlem  44499  liminfequzmpt2  44555  cncficcgt0  44652  cncfioobd  44661  fprodsubrecnncnvlem  44671  fprodaddrecnncnvlem  44673  dvmptfprodlem  44708  dvnprodlem1  44710  iblsplitf  44734  stoweidlem5  44769  stoweidlem16  44780  stoweidlem18  44782  stoweidlem21  44785  stoweidlem26  44790  stoweidlem27  44791  stoweidlem28  44792  stoweidlem29  44793  stoweidlem31  44795  stoweidlem34  44798  stoweidlem36  44800  stoweidlem41  44805  stoweidlem42  44806  stoweidlem44  44808  stoweidlem45  44809  stoweidlem48  44812  stoweidlem51  44815  stoweidlem55  44819  stoweidlem59  44823  stoweidlem60  44824  stoweidlem62  44826  wallispilem3  44831  stirlinglem5  44842  fourierdlem16  44887  fourierdlem21  44892  fourierdlem22  44893  fourierdlem31  44902  fourierdlem39  44910  fourierdlem68  44938  fourierdlem71  44941  fourierdlem73  44943  fourierdlem77  44947  fourierdlem80  44950  fourierdlem83  44953  fourierdlem87  44957  fourierdlem94  44964  fourierdlem103  44973  fourierdlem104  44974  fourierdlem112  44982  fourierdlem113  44983  etransclem32  45030  subsaliuncllem  45121  sge0revalmpt  45142  sge0fodjrnlem  45180  sge0fsummptf  45200  iundjiun  45224  meadjiun  45230  voliunsge0lem  45236  meaiininclem  45250  omeiunle  45281  hoicvrrex  45320  ovnsubaddlem2  45335  hoissrrn2  45342  hoidmv1lelem1  45355  hoidmvlelem3  45361  ovnhoilem1  45365  hoi2toco  45371  ovnlecvr2  45374  hspdifhsp  45380  hoiqssbllem1  45386  hoiqssbllem3  45388  hspmbllem2  45391  iinhoiicclem  45437  iunhoiioolem  45439  vonioo  45446  vonicc  45449  pimconstlt0  45465  pimconstlt1  45466  pimltpnff  45467  pimiooltgt  45474  pimdecfgtioc  45479  pimincfltioc  45480  pimdecfgtioo  45481  pimincfltioo  45482  preimageiingt  45484  preimaleiinlt  45485  pimgtmnff  45486  issmfd  45499  issmfdf  45501  sssmf  45502  issmfle  45509  issmfdmpt  45512  issmfgt  45520  issmfled  45521  issmfgtd  45525  smflimlem2  45536  smfmullem4  45558  smfpimcclem  45571  smfsuplem1  45575  smfinflem  45581  smfinfmpt  45583  iccelpart  46149  mogoldbb  46501  sbgoldbo  46503  pgindnf  47809  aacllem  47896