Theorem ralrimi 3269

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

Syntax hints:   → wi 4  Ⅎwnf 1810   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811  df-ral 3086

This theorem is referenced by:  ralrimia  3270  reximdai  3273  r19.37  3274  rexlimd2  3277  r19.12  3320  ralcom2  3372  2rmorex  3724  disjxiun  5108  nelrnmpt  5958  rnmpt0f  6245  fnmptd  6677  mpteqb  7010  fmptdf  7113  eusvobj2  7403  offval2f  7690  zfrep6OLD  7952  frrlem4  8286  tfr3  8386  tz7.49  8432  mapxpen  9131  dfac2b  10114  hsmexlem4  10413  axcc3  10422  domtriomlem  10426  axdc3lem2  10435  axdc3lem4  10437  axdc4lem  10439  ac6num  10463  dedekind  11373  dedekindle  11374  fsuppmapnn0fiublem  14026  fsuppmapnn0fiub  14027  fprodcllemf  16012  lcmfunsnlem1  16695  lcmfunsnlem2lem1  16696  lcmfunsnlem2  16698  mreexexd  17704  cpmatmcllem  22844  ptcnplem  23747  xkocnv  23940  cfilucfil  24685  cncfcompt2  25036  itg2splitlem  25876  itg2split  25877  itgeq1fOLD  25900  bdaypw2n0bndlem  28622  mpteleeOLD  29186  lfgrnloop  29416  foresf1o  32791  iinabrex  32855  funimass4f  32923  fcomptf  32944  aciunf1lem  32948  fnpreimac  32956  prodindf  33123  isarchiofld  33460  reff  34174  locfinreflem  34175  zarclsiin  34206  zarcmplem  34216  esumeq12dvaf  34366  esumgsum  34380  esumel  34382  esumf1o  34385  esumc  34386  esummono  34389  gsumesum  34394  esumlub  34395  esumlef  34397  esumfsup  34405  esumpinfval  34408  esumpinfsum  34412  esum2d  34428  ldsysgenld  34495  sigapildsyslem  34496  ldgenpisyslem1  34498  measinblem  34555  voliune  34564  volmeas  34566  oms0  34632  omssubadd  34635  dstrvprob  34807  bnj1379  35163  bnj1204  35345  bnj1388  35366  bnj1417  35374  bnj1489  35389  untsucf  36135  domalom  37973  fvineqsneq  37981  cover2  38289  upixp  38303  indexdom  38308  filbcmb  38314  sdclem2  38316  eq0rabdioph  43434  eqrabdioph  43435  setindtr  43678  gneispace  44787  mnuprdlem3  44911  iunconnlem2  45570  rzalf  45664  fnchoice  45676  refsumcn  45677  rfcnnnub  45683  refsum2cnlem1  45684  iuneq2df  45694  uzwo4  45700  ixpeq2d  45715  ixpssmapc  45720  elintd  45721  ssdf  45722  ralimralim  45728  ixpssixp  45737  ballss3  45738  iinssiin  45774  eliind2  45775  rabssd  45787  choicefi  45844  iunmapss  45858  iunmapsn  45860  axccdom  45865  mptfnd  45884  ssfiunibd  45955  xralrple2  45997  infxr  46009  xrralrecnnle  46025  xrralrecnnge  46032  supxrunb3  46041  fimaxre4  46042  supxrleubrnmpt  46047  rexabslelem  46059  suprleubrnmpt  46063  uzublem  46071  infxrgelbrnmpt  46095  iooiinicc  46185  iooiinioc  46199  mccl  46241  climsuse  46251  mullimc  46259  mullimcf  46266  limcrecl  46272  limsupre  46282  limcleqr  46285  addlimc  46289  0ellimcdiv  46290  limclner  46292  limsupubuzlem  46353  climinf3  46357  limsupequzmpt2  46359  limsupmnfuzlem  46367  limsupre3uzlem  46376  liminfequzmpt2  46432  cncficcgt0  46529  cncfioobd  46538  fprodsubrecnncnvlem  46548  fprodaddrecnncnvlem  46550  dvmptfprodlem  46585  dvnprodlem1  46587  iblsplitf  46611  stoweidlem5  46646  stoweidlem16  46657  stoweidlem18  46659  stoweidlem21  46662  stoweidlem26  46667  stoweidlem27  46668  stoweidlem28  46669  stoweidlem29  46670  stoweidlem31  46672  stoweidlem34  46675  stoweidlem36  46677  stoweidlem41  46682  stoweidlem42  46683  stoweidlem44  46685  stoweidlem45  46686  stoweidlem48  46689  stoweidlem51  46692  stoweidlem55  46696  stoweidlem59  46700  stoweidlem60  46701  stoweidlem62  46703  wallispilem3  46708  stirlinglem5  46719  fourierdlem16  46764  fourierdlem21  46769  fourierdlem22  46770  fourierdlem31  46779  fourierdlem39  46787  fourierdlem68  46815  fourierdlem71  46818  fourierdlem73  46820  fourierdlem77  46824  fourierdlem80  46827  fourierdlem83  46830  fourierdlem87  46834  fourierdlem94  46841  fourierdlem103  46850  fourierdlem104  46851  fourierdlem112  46859  etransclem32  46907  subsaliuncllem  46998  sge0revalmpt  47019  sge0fodjrnlem  47057  sge0fsummptf  47077  iundjiun  47101  meadjiun  47107  voliunsge0lem  47113  meaiininclem  47127  omeiunle  47158  hoicvrrex  47197  ovnsubaddlem2  47212  hoissrrn2  47219  hoidmv1lelem1  47232  hoidmvlelem3  47238  ovnhoilem1  47242  hoi2toco  47248  ovnlecvr2  47251  hspdifhsp  47257  hoiqssbllem1  47263  hoiqssbllem3  47265  hspmbllem2  47268  iinhoiicclem  47314  iunhoiioolem  47316  vonioo  47323  vonicc  47326  pimconstlt0  47342  pimconstlt1  47343  pimltpnff  47344  pimiooltgt  47351  pimdecfgtioc  47356  pimincfltioc  47357  pimdecfgtioo  47358  pimincfltioo  47359  pimgtmnff  47363  issmfd  47376  issmfdf  47378  issmfle  47386  issmfdmpt  47389  issmfgt  47397  issmfled  47398  issmfgtd  47402  smflimlem2  47413  smfmullem4  47435  smfpimcclem  47448  smfsuplem1  47452  smfinflem  47458  iccelpart  48106  mogoldbb  48474  sbgoldbo  48476  pgindnf  50414  aacllem  50510