Theorem ralrimi 3227

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-ral 3045

This theorem is referenced by:  ralrimia  3228  ralimdaa  3230  reximdai  3231  r19.37  3232  rexlimd2  3235  r19.12  3278  ralcom2  3340  rabbidaOLD  3433  2rmorex  3714  iineq2d  4965  disjxiun  5089  rnmpt0f  6192  fnmptd  6623  mpteqb  6949  fmptdf  7051  eusvobj2  7341  offval2f  7628  zfrep6  7890  frrlem4  8222  tfr3  8321  tz7.49  8367  mapxpen  9060  dfac2b  10025  hsmexlem4  10323  axcc3  10332  domtriomlem  10336  axdc3lem2  10345  axdc3lem4  10347  axdc4lem  10349  ac6num  10373  dedekind  11279  dedekindle  11280  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  fprodcllemf  15865  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  mreexexd  17554  cpmatmcllem  22603  ptcnplem  23506  xkocnv  23699  cfilucfil  24445  cncfcompt2  24799  itg2splitlem  25647  itg2split  25648  itgeq1fOLD  25671  mptelee  28844  lfgrnloop  29074  foresf1o  32453  iinabrex  32518  funimass4f  32588  fcomptf  32609  aciunf1lem  32613  funcnvmpt  32618  fnpreimac  32622  prodindf  32815  isarchiofld  33150  reff  33822  locfinreflem  33823  zarclsiin  33854  zarcmplem  33864  esumeq12dvaf  34014  esumgsum  34028  esumel  34030  esumf1o  34033  esumc  34034  esummono  34037  gsumesum  34042  esumlub  34043  esumlef  34045  esumfsup  34053  esumpinfval  34056  esumpinfsum  34060  esum2d  34076  ldsysgenld  34143  sigapildsyslem  34144  ldgenpisyslem1  34146  measinblem  34203  voliune  34212  volmeas  34214  oms0  34281  omssubadd  34284  dstrvprob  34456  bnj1379  34813  bnj1204  34995  bnj1388  35016  bnj1417  35024  bnj1489  35039  untsucf  35703  domalom  37398  fvineqsneq  37406  cover2  37715  upixp  37729  indexdom  37734  filbcmb  37740  sdclem2  37742  eq0rabdioph  42769  eqrabdioph  42770  setindtr  43017  gneispace  44127  mnuprdlem3  44267  iunconnlem2  44928  rzalf  45015  fnchoice  45027  refsumcn  45028  rfcnnnub  45034  refsum2cnlem1  45035  iuneq2df  45045  uzwo4  45051  ixpeq2d  45066  ixpssmapc  45071  elintd  45072  ssdf  45073  ralimralim  45079  nelrnmpt  45082  ixpssixp  45090  ballss3  45091  iinssiin  45127  eliind2  45128  rabssd  45140  ss2rabdf  45148  choicefi  45198  iunmapss  45213  iunmapsn  45215  axccdom  45220  mptfnd  45240  ssfiunibd  45311  xralrple2  45354  infxr  45366  xrralrecnnle  45382  xrralrecnnge  45389  supxrunb3  45398  fimaxre4  45400  supxrleubrnmpt  45405  rexabslelem  45417  suprleubrnmpt  45421  uzublem  45429  infxrgelbrnmpt  45453  iooiinicc  45543  iooiinioc  45557  mccl  45599  climsuse  45609  mullimc  45617  mullimcf  45624  limcrecl  45630  limsupre  45642  limcleqr  45645  addlimc  45649  0ellimcdiv  45650  limclner  45652  limsupubuzlem  45713  climinf3  45717  limsupequzmpt2  45719  limsupmnfuzlem  45727  limsupre3uzlem  45736  liminfequzmpt2  45792  cncficcgt0  45889  cncfioobd  45898  fprodsubrecnncnvlem  45908  fprodaddrecnncnvlem  45910  dvmptfprodlem  45945  dvnprodlem1  45947  iblsplitf  45971  stoweidlem5  46006  stoweidlem16  46017  stoweidlem18  46019  stoweidlem21  46022  stoweidlem26  46027  stoweidlem27  46028  stoweidlem28  46029  stoweidlem29  46030  stoweidlem31  46032  stoweidlem34  46035  stoweidlem36  46037  stoweidlem41  46042  stoweidlem42  46043  stoweidlem44  46045  stoweidlem45  46046  stoweidlem48  46049  stoweidlem51  46052  stoweidlem55  46056  stoweidlem59  46060  stoweidlem60  46061  stoweidlem62  46063  wallispilem3  46068  stirlinglem5  46079  fourierdlem16  46124  fourierdlem21  46129  fourierdlem22  46130  fourierdlem31  46139  fourierdlem39  46147  fourierdlem68  46175  fourierdlem71  46178  fourierdlem73  46180  fourierdlem77  46184  fourierdlem80  46187  fourierdlem83  46190  fourierdlem87  46194  fourierdlem94  46201  fourierdlem103  46210  fourierdlem104  46211  fourierdlem112  46219  fourierdlem113  46220  etransclem32  46267  subsaliuncllem  46358  sge0revalmpt  46379  sge0fodjrnlem  46417  sge0fsummptf  46437  iundjiun  46461  meadjiun  46467  voliunsge0lem  46473  meaiininclem  46487  omeiunle  46518  hoicvrrex  46557  ovnsubaddlem2  46572  hoissrrn2  46579  hoidmv1lelem1  46592  hoidmvlelem3  46598  ovnhoilem1  46602  hoi2toco  46608  ovnlecvr2  46611  hspdifhsp  46617  hoiqssbllem1  46623  hoiqssbllem3  46625  hspmbllem2  46628  iinhoiicclem  46674  iunhoiioolem  46676  vonioo  46683  vonicc  46686  pimconstlt0  46702  pimconstlt1  46703  pimltpnff  46704  pimiooltgt  46711  pimdecfgtioc  46716  pimincfltioc  46717  pimdecfgtioo  46718  pimincfltioo  46719  preimageiingt  46721  preimaleiinlt  46722  pimgtmnff  46723  issmfd  46736  issmfdf  46738  sssmf  46739  issmfle  46746  issmfdmpt  46749  issmfgt  46757  issmfled  46758  issmfgtd  46762  smflimlem2  46773  smfmullem4  46795  smfpimcclem  46808  smfsuplem1  46812  smfinflem  46818  iccelpart  47437  mogoldbb  47789  sbgoldbo  47791  pgindnf  49721  aacllem  49806