Theorem ralrimi 3234

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785  df-ral 3052

This theorem is referenced by:  ralrimia  3235  ralimdaa  3237  reximdai  3238  r19.37  3239  rexlimd2  3242  r19.12  3285  ralcom2  3347  rabbidaOLD  3437  2rmorex  3712  iineq2d  4970  disjxiun  5095  nelrnmpt  5916  rnmpt0f  6201  fnmptd  6633  mpteqb  6960  fmptdf  7062  eusvobj2  7350  offval2f  7637  zfrep6  7899  frrlem4  8231  tfr3  8330  tz7.49  8376  mapxpen  9071  dfac2b  10041  hsmexlem4  10339  axcc3  10348  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  ac6num  10389  dedekind  11296  dedekindle  11297  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  fprodcllemf  15881  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem2  16567  mreexexd  17571  cpmatmcllem  22662  ptcnplem  23565  xkocnv  23758  cfilucfil  24503  cncfcompt2  24857  itg2splitlem  25705  itg2split  25706  itgeq1fOLD  25729  bdaypw2n0bndlem  28459  mpteleeOLD  28968  lfgrnloop  29198  foresf1o  32579  iinabrex  32644  funimass4f  32715  fcomptf  32736  aciunf1lem  32740  funcnvmpt  32745  fnpreimac  32749  prodindf  32944  isarchiofld  33281  reff  33996  locfinreflem  33997  zarclsiin  34028  zarcmplem  34038  esumeq12dvaf  34188  esumgsum  34202  esumel  34204  esumf1o  34207  esumc  34208  esummono  34211  gsumesum  34216  esumlub  34217  esumlef  34219  esumfsup  34227  esumpinfval  34230  esumpinfsum  34234  esum2d  34250  ldsysgenld  34317  sigapildsyslem  34318  ldgenpisyslem1  34320  measinblem  34377  voliune  34386  volmeas  34388  oms0  34454  omssubadd  34457  dstrvprob  34629  bnj1379  34986  bnj1204  35168  bnj1388  35189  bnj1417  35197  bnj1489  35212  untsucf  35904  domalom  37609  fvineqsneq  37617  cover2  37916  upixp  37930  indexdom  37935  filbcmb  37941  sdclem2  37943  eq0rabdioph  43018  eqrabdioph  43019  setindtr  43266  gneispace  44375  mnuprdlem3  44515  iunconnlem2  45175  rzalf  45262  fnchoice  45274  refsumcn  45275  rfcnnnub  45281  refsum2cnlem1  45282  iuneq2df  45292  uzwo4  45298  ixpeq2d  45313  ixpssmapc  45318  elintd  45319  ssdf  45320  ralimralim  45326  ixpssixp  45336  ballss3  45337  iinssiin  45373  eliind2  45374  rabssd  45386  choicefi  45444  iunmapss  45459  iunmapsn  45461  axccdom  45466  mptfnd  45486  ssfiunibd  45557  xralrple2  45599  infxr  45611  xrralrecnnle  45627  xrralrecnnge  45634  supxrunb3  45643  fimaxre4  45645  supxrleubrnmpt  45650  rexabslelem  45662  suprleubrnmpt  45666  uzublem  45674  infxrgelbrnmpt  45698  iooiinicc  45788  iooiinioc  45802  mccl  45844  climsuse  45854  mullimc  45862  mullimcf  45869  limcrecl  45875  limsupre  45885  limcleqr  45888  addlimc  45892  0ellimcdiv  45893  limclner  45895  limsupubuzlem  45956  climinf3  45960  limsupequzmpt2  45962  limsupmnfuzlem  45970  limsupre3uzlem  45979  liminfequzmpt2  46035  cncficcgt0  46132  cncfioobd  46141  fprodsubrecnncnvlem  46151  fprodaddrecnncnvlem  46153  dvmptfprodlem  46188  dvnprodlem1  46190  iblsplitf  46214  stoweidlem5  46249  stoweidlem16  46260  stoweidlem18  46262  stoweidlem21  46265  stoweidlem26  46270  stoweidlem27  46271  stoweidlem28  46272  stoweidlem29  46273  stoweidlem31  46275  stoweidlem34  46278  stoweidlem36  46280  stoweidlem41  46285  stoweidlem42  46286  stoweidlem44  46288  stoweidlem45  46289  stoweidlem48  46292  stoweidlem51  46295  stoweidlem55  46299  stoweidlem59  46303  stoweidlem60  46304  stoweidlem62  46306  wallispilem3  46311  stirlinglem5  46322  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem31  46382  fourierdlem39  46390  fourierdlem68  46418  fourierdlem71  46421  fourierdlem73  46423  fourierdlem77  46427  fourierdlem80  46430  fourierdlem83  46433  fourierdlem87  46437  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  fourierdlem113  46463  etransclem32  46510  subsaliuncllem  46601  sge0revalmpt  46622  sge0fodjrnlem  46660  sge0fsummptf  46680  iundjiun  46704  meadjiun  46710  voliunsge0lem  46716  meaiininclem  46730  omeiunle  46761  hoicvrrex  46800  ovnsubaddlem2  46815  hoissrrn2  46822  hoidmv1lelem1  46835  hoidmvlelem3  46841  ovnhoilem1  46845  hoi2toco  46851  ovnlecvr2  46854  hspdifhsp  46860  hoiqssbllem1  46866  hoiqssbllem3  46868  hspmbllem2  46871  iinhoiicclem  46917  iunhoiioolem  46919  vonioo  46926  vonicc  46929  pimconstlt0  46945  pimconstlt1  46946  pimltpnff  46947  pimiooltgt  46954  pimdecfgtioc  46959  pimincfltioc  46960  pimdecfgtioo  46961  pimincfltioo  46962  pimgtmnff  46966  issmfd  46979  issmfdf  46981  sssmf  46982  issmfle  46989  issmfdmpt  46992  issmfgt  47000  issmfled  47001  issmfgtd  47005  smflimlem2  47016  smfmullem4  47038  smfpimcclem  47051  smfsuplem1  47055  smfinflem  47061  iccelpart  47679  mogoldbb  48031  sbgoldbo  48033  pgindnf  49961  aacllem  50046