Theorem ralrimi 3141

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3101. (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 2188	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		ralrimi.2	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	2, 3	hbralrimi 3101	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1786   ∈ wcel 2106  ∀wral 3064

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

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

This theorem is referenced by:  ralimdaa  3142  reximdai  3244  rexlimd2  3249  r19.12  3257  r19.12OLD  3258  r19.37  3273  ralcom2  3290  rabbida  3409  ralrimia  3430  2rmorex  3689  iineq2d  4947  disjxiun  5071  mpteq2daOLD  5173  rnmpt0f  6146  fnmptd  6574  mpteqb  6894  fmptdf  6991  eusvobj2  7268  offval2f  7548  zfrep6  7797  frrlem4  8105  wfrlem4OLD  8143  tfr3  8230  tz7.49  8276  mapxpen  8930  dfac2b  9886  hsmexlem4  10185  axcc3  10194  domtriomlem  10198  axdc3lem2  10207  axdc3lem4  10209  axdc4lem  10211  ac6num  10235  dedekind  11138  dedekindle  11139  fsuppmapnn0fiublem  13710  fsuppmapnn0fiub  13711  fprodcllemf  15668  lcmfunsnlem1  16342  lcmfunsnlem2lem1  16343  lcmfunsnlem2  16345  mreexexd  17357  cpmatmcllem  21867  ptcnplem  22772  xkocnv  22965  cfilucfil  23715  cncfcompt2  24071  itg2splitlem  24913  itg2split  24914  itgeq1f  24936  mptelee  27263  lfgrnloop  27495  foresf1o  30850  iinabrex  30908  funimass4f  30972  fcomptf  30995  aciunf1lem  30999  funcnvmpt  31004  fnpreimac  31008  isarchiofld  31516  reff  31789  locfinreflem  31790  zarclsiin  31821  zarcmplem  31831  prodindf  31991  esumeq12dvaf  31999  esumgsum  32013  esumel  32015  esumf1o  32018  esumc  32019  esummono  32022  gsumesum  32027  esumlub  32028  esumlef  32030  esumfsup  32038  esumpinfval  32041  esumpinfsum  32045  esum2d  32061  ldsysgenld  32128  sigapildsyslem  32129  ldgenpisyslem1  32131  measinblem  32188  voliune  32197  volmeas  32199  oms0  32264  omssubadd  32267  dstrvprob  32438  bnj1379  32810  bnj1204  32992  bnj1388  33013  bnj1417  33021  bnj1489  33036  untsucf  33651  domalom  35575  fvineqsneq  35583  cover2  35872  upixp  35887  indexdom  35892  filbcmb  35898  sdclem2  35900  eq0rabdioph  40598  eqrabdioph  40599  setindtr  40846  ss2iundf  41267  gneispace  41744  mnuprdlem3  41892  iunconnlem2  42555  rzalf  42560  fnchoice  42572  refsumcn  42573  rfcnnnub  42579  refsum2cnlem1  42580  iuneq2df  42594  uzwo4  42601  ixpeq2d  42616  ixpssmapc  42622  elintd  42624  ssdf  42625  ralimralim  42631  nelrnmpt  42634  ixpssixp  42642  ballss3  42643  iinssiin  42678  eliind2  42679  rabssd  42691  fompt  42730  choicefi  42740  iunmapss  42755  iunmapsn  42757  axccdom  42762  mptfnd  42786  ssfiunibd  42848  xralrple2  42893  infxr  42906  xrralrecnnle  42922  xrralrecnnge  42930  supxrunb3  42939  fimaxre4  42941  supxrleubrnmpt  42946  rexabslelem  42958  suprleubrnmpt  42962  uzublem  42970  infxrgelbrnmpt  42994  iooiinicc  43080  iooiinioc  43094  mccl  43139  climsuse  43149  mullimc  43157  mullimcf  43164  limcrecl  43170  limsupre  43182  limcleqr  43185  addlimc  43189  0ellimcdiv  43190  limclner  43192  limsupubuzlem  43253  climinf3  43257  limsupequzmpt2  43259  limsupmnfuzlem  43267  limsupre3uzlem  43276  liminfequzmpt2  43332  cncficcgt0  43429  cncfioobd  43438  fprodsubrecnncnvlem  43448  fprodaddrecnncnvlem  43450  dvmptfprodlem  43485  dvnprodlem1  43487  iblsplitf  43511  stoweidlem5  43546  stoweidlem16  43557  stoweidlem18  43559  stoweidlem21  43562  stoweidlem26  43567  stoweidlem27  43568  stoweidlem28  43569  stoweidlem29  43570  stoweidlem31  43572  stoweidlem34  43575  stoweidlem36  43577  stoweidlem41  43582  stoweidlem42  43583  stoweidlem44  43585  stoweidlem45  43586  stoweidlem48  43589  stoweidlem51  43592  stoweidlem55  43596  stoweidlem59  43600  stoweidlem60  43601  stoweidlem62  43603  wallispilem3  43608  stirlinglem5  43619  fourierdlem16  43664  fourierdlem21  43669  fourierdlem22  43670  fourierdlem31  43679  fourierdlem39  43687  fourierdlem68  43715  fourierdlem71  43718  fourierdlem73  43720  fourierdlem77  43724  fourierdlem80  43727  fourierdlem83  43730  fourierdlem87  43734  fourierdlem94  43741  fourierdlem103  43750  fourierdlem104  43751  fourierdlem112  43759  fourierdlem113  43760  etransclem32  43807  subsaliuncllem  43896  sge0revalmpt  43916  sge0fodjrnlem  43954  sge0fsummptf  43974  iundjiun  43998  meadjiun  44004  voliunsge0lem  44010  meaiininclem  44024  omeiunle  44055  hoicvrrex  44094  ovnsubaddlem2  44109  hoissrrn2  44116  hoidmv1lelem1  44129  hoidmvlelem3  44135  ovnhoilem1  44139  hoi2toco  44145  ovnlecvr2  44148  hspdifhsp  44154  hoiqssbllem1  44160  hoiqssbllem3  44162  hspmbllem2  44165  iinhoiicclem  44211  iunhoiioolem  44213  vonioo  44220  vonicc  44223  pimconstlt0  44239  pimconstlt1  44240  pimltpnf  44241  pimiooltgt  44247  pimdecfgtioc  44252  pimincfltioc  44253  pimdecfgtioo  44254  pimincfltioo  44255  preimageiingt  44257  preimaleiinlt  44258  issmfd  44271  issmfdf  44273  sssmf  44274  issmfle  44281  issmfdmpt  44284  issmfgt  44292  issmfled  44293  issmfgtd  44296  smflimlem2  44307  smfmullem4  44328  smfpimcclem  44340  smfsuplem1  44344  smfinflem  44350  smfinfmpt  44352  iccelpart  44885  mogoldbb  45237  sbgoldbo  45239  aacllem  46505