Theorem ralrimi 3235

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). For a version based on fewer axioms see ralrimiv 3124. (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3123. (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 3123	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  3236  ralimdaa  3238  reximdai  3239  r19.37  3240  rexlimd2  3243  r19.12  3288  ralcom2  3351  rabbidaOLD  3444  2rmorex  3725  iineq2d  4979  disjxiun  5104  rnmpt0f  6216  fnmptd  6659  mpteqb  6987  fmptdf  7089  eusvobj2  7379  offval2f  7668  zfrep6  7933  frrlem4  8268  tfr3  8367  tz7.49  8413  mapxpen  9107  dfac2b  10084  hsmexlem4  10382  axcc3  10391  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  ac6num  10432  dedekind  11337  dedekindle  11338  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fprodcllemf  15924  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  mreexexd  17609  cpmatmcllem  22605  ptcnplem  23508  xkocnv  23701  cfilucfil  24447  cncfcompt2  24801  itg2splitlem  25649  itg2split  25650  itgeq1fOLD  25673  mptelee  28822  lfgrnloop  29052  foresf1o  32433  iinabrex  32498  funimass4f  32561  fcomptf  32582  aciunf1lem  32586  funcnvmpt  32591  fnpreimac  32595  prodindf  32786  isarchiofld  33295  reff  33829  locfinreflem  33830  zarclsiin  33861  zarcmplem  33871  esumeq12dvaf  34021  esumgsum  34035  esumel  34037  esumf1o  34040  esumc  34041  esummono  34044  gsumesum  34049  esumlub  34050  esumlef  34052  esumfsup  34060  esumpinfval  34063  esumpinfsum  34067  esum2d  34083  ldsysgenld  34150  sigapildsyslem  34151  ldgenpisyslem1  34153  measinblem  34210  voliune  34219  volmeas  34221  oms0  34288  omssubadd  34291  dstrvprob  34463  bnj1379  34820  bnj1204  35002  bnj1388  35023  bnj1417  35031  bnj1489  35046  untsucf  35697  domalom  37392  fvineqsneq  37400  cover2  37709  upixp  37723  indexdom  37728  filbcmb  37734  sdclem2  37736  eq0rabdioph  42764  eqrabdioph  42765  setindtr  43013  gneispace  44123  mnuprdlem3  44263  iunconnlem2  44924  rzalf  45011  fnchoice  45023  refsumcn  45024  rfcnnnub  45030  refsum2cnlem1  45031  iuneq2df  45041  uzwo4  45047  ixpeq2d  45062  ixpssmapc  45067  elintd  45068  ssdf  45069  ralimralim  45075  nelrnmpt  45078  ixpssixp  45086  ballss3  45087  iinssiin  45123  eliind2  45124  rabssd  45136  ss2rabdf  45144  choicefi  45194  iunmapss  45209  iunmapsn  45211  axccdom  45216  mptfnd  45236  ssfiunibd  45307  xralrple2  45350  infxr  45363  xrralrecnnle  45379  xrralrecnnge  45386  supxrunb3  45395  fimaxre4  45397  supxrleubrnmpt  45402  rexabslelem  45414  suprleubrnmpt  45418  uzublem  45426  infxrgelbrnmpt  45450  iooiinicc  45540  iooiinioc  45554  mccl  45596  climsuse  45606  mullimc  45614  mullimcf  45621  limcrecl  45627  limsupre  45639  limcleqr  45642  addlimc  45646  0ellimcdiv  45647  limclner  45649  limsupubuzlem  45710  climinf3  45714  limsupequzmpt2  45716  limsupmnfuzlem  45724  limsupre3uzlem  45733  liminfequzmpt2  45789  cncficcgt0  45886  cncfioobd  45895  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  dvmptfprodlem  45942  dvnprodlem1  45944  iblsplitf  45968  stoweidlem5  46003  stoweidlem16  46014  stoweidlem18  46016  stoweidlem21  46019  stoweidlem26  46024  stoweidlem27  46025  stoweidlem28  46026  stoweidlem29  46027  stoweidlem31  46029  stoweidlem34  46032  stoweidlem36  46034  stoweidlem41  46039  stoweidlem42  46040  stoweidlem44  46042  stoweidlem45  46043  stoweidlem48  46046  stoweidlem51  46049  stoweidlem55  46053  stoweidlem59  46057  stoweidlem60  46058  stoweidlem62  46060  wallispilem3  46065  stirlinglem5  46076  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem31  46136  fourierdlem39  46144  fourierdlem68  46172  fourierdlem71  46175  fourierdlem73  46177  fourierdlem77  46181  fourierdlem80  46184  fourierdlem83  46187  fourierdlem87  46191  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  etransclem32  46264  subsaliuncllem  46355  sge0revalmpt  46376  sge0fodjrnlem  46414  sge0fsummptf  46434  iundjiun  46458  meadjiun  46464  voliunsge0lem  46470  meaiininclem  46484  omeiunle  46515  hoicvrrex  46554  ovnsubaddlem2  46569  hoissrrn2  46576  hoidmv1lelem1  46589  hoidmvlelem3  46595  ovnhoilem1  46599  hoi2toco  46605  ovnlecvr2  46608  hspdifhsp  46614  hoiqssbllem1  46620  hoiqssbllem3  46622  hspmbllem2  46625  iinhoiicclem  46671  iunhoiioolem  46673  vonioo  46680  vonicc  46683  pimconstlt0  46699  pimconstlt1  46700  pimltpnff  46701  pimiooltgt  46708  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  preimageiingt  46718  preimaleiinlt  46719  pimgtmnff  46720  issmfd  46733  issmfdf  46735  sssmf  46736  issmfle  46743  issmfdmpt  46746  issmfgt  46754  issmfled  46755  issmfgtd  46759  smflimlem2  46770  smfmullem4  46792  smfpimcclem  46805  smfsuplem1  46809  smfinflem  46815  iccelpart  47434  mogoldbb  47786  sbgoldbo  47788  pgindnf  49705  aacllem  49790