Theorem ralrimi 3239

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

Syntax hints:   → wi 4  Ⅎwnf 1791   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-ex 1788  df-nf 1792  df-ral 3056

This theorem is referenced by:  ralrimia  3240  reximdai  3243  r19.37  3244  rexlimd2  3247  r19.12  3290  ralcom2  3343  2rmorex  3697  disjxiun  5072  nelrnmpt  5916  rnmpt0f  6198  fnmptd  6630  mpteqb  6959  fmptdf  7062  eusvobj2  7352  offval2f  7639  zfrep6OLD  7901  frrlem4  8233  tfr3  8332  tz7.49  8378  mapxpen  9075  dfac2b  10048  hsmexlem4  10346  axcc3  10355  domtriomlem  10359  axdc3lem2  10368  axdc3lem4  10370  axdc4lem  10372  ac6num  10396  dedekind  11304  dedekindle  11305  fsuppmapnn0fiublem  13947  fsuppmapnn0fiub  13948  fprodcllemf  15918  lcmfunsnlem1  16601  lcmfunsnlem2lem1  16602  lcmfunsnlem2  16604  mreexexd  17609  cpmatmcllem  22705  ptcnplem  23608  xkocnv  23801  cfilucfil  24546  cncfcompt2  24897  itg2splitlem  25737  itg2split  25738  itgeq1fOLD  25761  bdaypw2n0bndlem  28477  mpteleeOLD  28986  lfgrnloop  29216  foresf1o  32596  iinabrex  32662  funimass4f  32733  fcomptf  32754  aciunf1lem  32758  fnpreimac  32766  prodindf  32945  isarchiofld  33284  reff  34035  locfinreflem  34036  zarclsiin  34067  zarcmplem  34077  esumeq12dvaf  34227  esumgsum  34241  esumel  34243  esumf1o  34246  esumc  34247  esummono  34250  gsumesum  34255  esumlub  34256  esumlef  34258  esumfsup  34266  esumpinfval  34269  esumpinfsum  34273  esum2d  34289  ldsysgenld  34356  sigapildsyslem  34357  ldgenpisyslem1  34359  measinblem  34416  voliune  34425  volmeas  34427  oms0  34493  omssubadd  34496  dstrvprob  34668  bnj1379  35027  bnj1204  35209  bnj1388  35230  bnj1417  35238  bnj1489  35253  untsucf  35953  domalom  37781  fvineqsneq  37789  cover2  38097  upixp  38111  indexdom  38116  filbcmb  38122  sdclem2  38124  eq0rabdioph  43240  eqrabdioph  43241  setindtr  43484  gneispace  44593  mnuprdlem3  44733  iunconnlem2  45393  rzalf  45480  fnchoice  45492  refsumcn  45493  rfcnnnub  45499  refsum2cnlem1  45500  iuneq2df  45510  uzwo4  45516  ixpeq2d  45531  ixpssmapc  45536  elintd  45537  ssdf  45538  ralimralim  45544  ixpssixp  45553  ballss3  45554  iinssiin  45590  eliind2  45591  rabssd  45603  choicefi  45660  iunmapss  45674  iunmapsn  45676  axccdom  45681  mptfnd  45700  ssfiunibd  45771  xralrple2  45813  infxr  45825  xrralrecnnle  45841  xrralrecnnge  45848  supxrunb3  45857  fimaxre4  45858  supxrleubrnmpt  45863  rexabslelem  45875  suprleubrnmpt  45879  uzublem  45887  infxrgelbrnmpt  45911  iooiinicc  46001  iooiinioc  46015  mccl  46057  climsuse  46067  mullimc  46075  mullimcf  46082  limcrecl  46088  limsupre  46098  limcleqr  46101  addlimc  46105  0ellimcdiv  46106  limclner  46108  limsupubuzlem  46169  climinf3  46173  limsupequzmpt2  46175  limsupmnfuzlem  46183  limsupre3uzlem  46192  liminfequzmpt2  46248  cncficcgt0  46345  cncfioobd  46354  fprodsubrecnncnvlem  46364  fprodaddrecnncnvlem  46366  dvmptfprodlem  46401  dvnprodlem1  46403  iblsplitf  46427  stoweidlem5  46462  stoweidlem16  46473  stoweidlem18  46475  stoweidlem21  46478  stoweidlem26  46483  stoweidlem27  46484  stoweidlem28  46485  stoweidlem29  46486  stoweidlem31  46488  stoweidlem34  46491  stoweidlem36  46493  stoweidlem41  46498  stoweidlem42  46499  stoweidlem44  46501  stoweidlem45  46502  stoweidlem48  46505  stoweidlem51  46508  stoweidlem55  46512  stoweidlem59  46516  stoweidlem60  46517  stoweidlem62  46519  wallispilem3  46524  stirlinglem5  46535  fourierdlem16  46580  fourierdlem21  46585  fourierdlem22  46586  fourierdlem31  46595  fourierdlem39  46603  fourierdlem68  46631  fourierdlem71  46634  fourierdlem73  46636  fourierdlem77  46640  fourierdlem80  46643  fourierdlem83  46646  fourierdlem87  46650  fourierdlem94  46657  fourierdlem103  46666  fourierdlem104  46667  fourierdlem112  46675  fourierdlem113  46676  etransclem32  46723  subsaliuncllem  46814  sge0revalmpt  46835  sge0fodjrnlem  46873  sge0fsummptf  46893  iundjiun  46917  meadjiun  46923  voliunsge0lem  46929  meaiininclem  46943  omeiunle  46974  hoicvrrex  47013  ovnsubaddlem2  47028  hoissrrn2  47035  hoidmv1lelem1  47048  hoidmvlelem3  47054  ovnhoilem1  47058  hoi2toco  47064  ovnlecvr2  47067  hspdifhsp  47073  hoiqssbllem1  47079  hoiqssbllem3  47081  hspmbllem2  47084  iinhoiicclem  47130  iunhoiioolem  47132  vonioo  47139  vonicc  47142  pimconstlt0  47158  pimconstlt1  47159  pimltpnff  47160  pimiooltgt  47167  pimdecfgtioc  47172  pimincfltioc  47173  pimdecfgtioo  47174  pimincfltioo  47175  pimgtmnff  47179  issmfd  47192  issmfdf  47194  sssmf  47195  issmfle  47202  issmfdmpt  47205  issmfgt  47213  issmfled  47214  issmfgtd  47218  smflimlem2  47229  smfmullem4  47251  smfpimcclem  47264  smfsuplem1  47268  smfinflem  47274  iccelpart  47922  mogoldbb  48290  sbgoldbo  48292  pgindnf  50220  aacllem  50305