Theorem ralrimi 3238

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2106  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786  df-ral 3061

This theorem is referenced by:  ralrimia  3239  ralimdaa  3241  reximdai  3242  r19.37  3243  rexlimd2  3246  r19.12  3295  r19.12OLD  3296  ralcom2  3348  rabbida  3431  2rmorex  3715  iineq2d  4982  disjxiun  5107  mpteq2daOLD  5209  rnmpt0f  6200  fnmptd  6647  mpteqb  6972  fmptdf  7070  eusvobj2  7354  offval2f  7637  zfrep6  7892  frrlem4  8225  wfrlem4OLD  8263  tfr3  8350  tz7.49  8396  mapxpen  9094  dfac2b  10075  hsmexlem4  10374  axcc3  10383  domtriomlem  10387  axdc3lem2  10396  axdc3lem4  10398  axdc4lem  10400  ac6num  10424  dedekind  11327  dedekindle  11328  fsuppmapnn0fiublem  13905  fsuppmapnn0fiub  13906  fprodcllemf  15852  lcmfunsnlem1  16524  lcmfunsnlem2lem1  16525  lcmfunsnlem2  16527  mreexexd  17542  cpmatmcllem  22104  ptcnplem  23009  xkocnv  23202  cfilucfil  23952  cncfcompt2  24308  itg2splitlem  25150  itg2split  25151  itgeq1f  25173  mptelee  27907  lfgrnloop  28139  foresf1o  31495  iinabrex  31554  funimass4f  31618  fcomptf  31641  aciunf1lem  31645  funcnvmpt  31650  fnpreimac  31654  isarchiofld  32183  reff  32509  locfinreflem  32510  zarclsiin  32541  zarcmplem  32551  prodindf  32711  esumeq12dvaf  32719  esumgsum  32733  esumel  32735  esumf1o  32738  esumc  32739  esummono  32742  gsumesum  32747  esumlub  32748  esumlef  32750  esumfsup  32758  esumpinfval  32761  esumpinfsum  32765  esum2d  32781  ldsysgenld  32848  sigapildsyslem  32849  ldgenpisyslem1  32851  measinblem  32908  voliune  32917  volmeas  32919  oms0  32986  omssubadd  32989  dstrvprob  33160  bnj1379  33531  bnj1204  33713  bnj1388  33734  bnj1417  33742  bnj1489  33757  untsucf  34368  domalom  35948  fvineqsneq  35956  cover2  36246  upixp  36261  indexdom  36266  filbcmb  36272  sdclem2  36274  eq0rabdioph  41157  eqrabdioph  41158  setindtr  41406  gneispace  42528  mnuprdlem3  42676  iunconnlem2  43339  rzalf  43344  fnchoice  43356  refsumcn  43357  rfcnnnub  43363  refsum2cnlem1  43364  iuneq2df  43376  uzwo4  43383  ixpeq2d  43398  ixpssmapc  43404  elintd  43406  ssdf  43407  ralimralim  43413  nelrnmpt  43416  ixpssixp  43424  ballss3  43425  iinssiin  43461  eliind2  43462  rabssd  43474  ss2rabdf  43487  fompt  43533  choicefi  43542  iunmapss  43557  iunmapsn  43559  axccdom  43564  mptfnd  43589  ssfiunibd  43664  xralrple2  43709  infxr  43722  xrralrecnnle  43738  xrralrecnnge  43745  supxrunb3  43754  fimaxre4  43756  supxrleubrnmpt  43761  rexabslelem  43773  suprleubrnmpt  43777  uzublem  43785  infxrgelbrnmpt  43809  iooiinicc  43900  iooiinioc  43914  mccl  43959  climsuse  43969  mullimc  43977  mullimcf  43984  limcrecl  43990  limsupre  44002  limcleqr  44005  addlimc  44009  0ellimcdiv  44010  limclner  44012  limsupubuzlem  44073  climinf3  44077  limsupequzmpt2  44079  limsupmnfuzlem  44087  limsupre3uzlem  44096  liminfequzmpt2  44152  cncficcgt0  44249  cncfioobd  44258  fprodsubrecnncnvlem  44268  fprodaddrecnncnvlem  44270  dvmptfprodlem  44305  dvnprodlem1  44307  iblsplitf  44331  stoweidlem5  44366  stoweidlem16  44377  stoweidlem18  44379  stoweidlem21  44382  stoweidlem26  44387  stoweidlem27  44388  stoweidlem28  44389  stoweidlem29  44390  stoweidlem31  44392  stoweidlem34  44395  stoweidlem36  44397  stoweidlem41  44402  stoweidlem42  44403  stoweidlem44  44405  stoweidlem45  44406  stoweidlem48  44409  stoweidlem51  44412  stoweidlem55  44416  stoweidlem59  44420  stoweidlem60  44421  stoweidlem62  44423  wallispilem3  44428  stirlinglem5  44439  fourierdlem16  44484  fourierdlem21  44489  fourierdlem22  44490  fourierdlem31  44499  fourierdlem39  44507  fourierdlem68  44535  fourierdlem71  44538  fourierdlem73  44540  fourierdlem77  44544  fourierdlem80  44547  fourierdlem83  44550  fourierdlem87  44554  fourierdlem94  44561  fourierdlem103  44570  fourierdlem104  44571  fourierdlem112  44579  fourierdlem113  44580  etransclem32  44627  subsaliuncllem  44718  sge0revalmpt  44739  sge0fodjrnlem  44777  sge0fsummptf  44797  iundjiun  44821  meadjiun  44827  voliunsge0lem  44833  meaiininclem  44847  omeiunle  44878  hoicvrrex  44917  ovnsubaddlem2  44932  hoissrrn2  44939  hoidmv1lelem1  44952  hoidmvlelem3  44958  ovnhoilem1  44962  hoi2toco  44968  ovnlecvr2  44971  hspdifhsp  44977  hoiqssbllem1  44983  hoiqssbllem3  44985  hspmbllem2  44988  iinhoiicclem  45034  iunhoiioolem  45036  vonioo  45043  vonicc  45046  pimconstlt0  45062  pimconstlt1  45063  pimltpnff  45064  pimiooltgt  45071  pimdecfgtioc  45076  pimincfltioc  45077  pimdecfgtioo  45078  pimincfltioo  45079  preimageiingt  45081  preimaleiinlt  45082  pimgtmnff  45083  issmfd  45096  issmfdf  45098  sssmf  45099  issmfle  45106  issmfdmpt  45109  issmfgt  45117  issmfled  45118  issmfgtd  45122  smflimlem2  45133  smfmullem4  45155  smfpimcclem  45168  smfsuplem1  45172  smfinflem  45178  smfinfmpt  45180  iccelpart  45745  mogoldbb  46097  sbgoldbo  46099  pgindnf  47281  aacllem  47368