Theorem ralrimi 3233

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  3234  ralimdaa  3236  reximdai  3237  r19.37  3238  rexlimd2  3241  r19.12  3285  ralcom2  3348  rabbidaOLD  3441  2rmorex  3722  iineq2d  4975  disjxiun  5099  rnmpt0f  6204  fnmptd  6641  mpteqb  6969  fmptdf  7071  eusvobj2  7361  offval2f  7648  zfrep6  7913  frrlem4  8245  tfr3  8344  tz7.49  8390  mapxpen  9084  dfac2b  10062  hsmexlem4  10360  axcc3  10369  domtriomlem  10373  axdc3lem2  10382  axdc3lem4  10384  axdc4lem  10386  ac6num  10410  dedekind  11315  dedekindle  11316  fsuppmapnn0fiublem  13933  fsuppmapnn0fiub  13934  fprodcllemf  15901  lcmfunsnlem1  16584  lcmfunsnlem2lem1  16585  lcmfunsnlem2  16587  mreexexd  17590  cpmatmcllem  22639  ptcnplem  23542  xkocnv  23735  cfilucfil  24481  cncfcompt2  24835  itg2splitlem  25683  itg2split  25684  itgeq1fOLD  25707  mptelee  28876  lfgrnloop  29106  foresf1o  32484  iinabrex  32549  funimass4f  32612  fcomptf  32633  aciunf1lem  32637  funcnvmpt  32642  fnpreimac  32646  prodindf  32837  isarchiofld  33169  reff  33823  locfinreflem  33824  zarclsiin  33855  zarcmplem  33865  esumeq12dvaf  34015  esumgsum  34029  esumel  34031  esumf1o  34034  esumc  34035  esummono  34038  gsumesum  34043  esumlub  34044  esumlef  34046  esumfsup  34054  esumpinfval  34057  esumpinfsum  34061  esum2d  34077  ldsysgenld  34144  sigapildsyslem  34145  ldgenpisyslem1  34147  measinblem  34204  voliune  34213  volmeas  34215  oms0  34282  omssubadd  34285  dstrvprob  34457  bnj1379  34814  bnj1204  34996  bnj1388  35017  bnj1417  35025  bnj1489  35040  untsucf  35691  domalom  37386  fvineqsneq  37394  cover2  37703  upixp  37717  indexdom  37722  filbcmb  37728  sdclem2  37730  eq0rabdioph  42758  eqrabdioph  42759  setindtr  43007  gneispace  44117  mnuprdlem3  44257  iunconnlem2  44918  rzalf  45005  fnchoice  45017  refsumcn  45018  rfcnnnub  45024  refsum2cnlem1  45025  iuneq2df  45035  uzwo4  45041  ixpeq2d  45056  ixpssmapc  45061  elintd  45062  ssdf  45063  ralimralim  45069  nelrnmpt  45072  ixpssixp  45080  ballss3  45081  iinssiin  45117  eliind2  45118  rabssd  45130  ss2rabdf  45138  choicefi  45188  iunmapss  45203  iunmapsn  45205  axccdom  45210  mptfnd  45230  ssfiunibd  45301  xralrple2  45344  infxr  45357  xrralrecnnle  45373  xrralrecnnge  45380  supxrunb3  45389  fimaxre4  45391  supxrleubrnmpt  45396  rexabslelem  45408  suprleubrnmpt  45412  uzublem  45420  infxrgelbrnmpt  45444  iooiinicc  45534  iooiinioc  45548  mccl  45590  climsuse  45600  mullimc  45608  mullimcf  45615  limcrecl  45621  limsupre  45633  limcleqr  45636  addlimc  45640  0ellimcdiv  45641  limclner  45643  limsupubuzlem  45704  climinf3  45708  limsupequzmpt2  45710  limsupmnfuzlem  45718  limsupre3uzlem  45727  liminfequzmpt2  45783  cncficcgt0  45880  cncfioobd  45889  fprodsubrecnncnvlem  45899  fprodaddrecnncnvlem  45901  dvmptfprodlem  45936  dvnprodlem1  45938  iblsplitf  45962  stoweidlem5  45997  stoweidlem16  46008  stoweidlem18  46010  stoweidlem21  46013  stoweidlem26  46018  stoweidlem27  46019  stoweidlem28  46020  stoweidlem29  46021  stoweidlem31  46023  stoweidlem34  46026  stoweidlem36  46028  stoweidlem41  46033  stoweidlem42  46034  stoweidlem44  46036  stoweidlem45  46037  stoweidlem48  46040  stoweidlem51  46043  stoweidlem55  46047  stoweidlem59  46051  stoweidlem60  46052  stoweidlem62  46054  wallispilem3  46059  stirlinglem5  46070  fourierdlem16  46115  fourierdlem21  46120  fourierdlem22  46121  fourierdlem31  46130  fourierdlem39  46138  fourierdlem68  46166  fourierdlem71  46169  fourierdlem73  46171  fourierdlem77  46175  fourierdlem80  46178  fourierdlem83  46181  fourierdlem87  46185  fourierdlem94  46192  fourierdlem103  46201  fourierdlem104  46202  fourierdlem112  46210  fourierdlem113  46211  etransclem32  46258  subsaliuncllem  46349  sge0revalmpt  46370  sge0fodjrnlem  46408  sge0fsummptf  46428  iundjiun  46452  meadjiun  46458  voliunsge0lem  46464  meaiininclem  46478  omeiunle  46509  hoicvrrex  46548  ovnsubaddlem2  46563  hoissrrn2  46570  hoidmv1lelem1  46583  hoidmvlelem3  46589  ovnhoilem1  46593  hoi2toco  46599  ovnlecvr2  46602  hspdifhsp  46608  hoiqssbllem1  46614  hoiqssbllem3  46616  hspmbllem2  46619  iinhoiicclem  46665  iunhoiioolem  46667  vonioo  46674  vonicc  46677  pimconstlt0  46693  pimconstlt1  46694  pimltpnff  46695  pimiooltgt  46702  pimdecfgtioc  46707  pimincfltioc  46708  pimdecfgtioo  46709  pimincfltioo  46710  preimageiingt  46712  preimaleiinlt  46713  pimgtmnff  46714  issmfd  46727  issmfdf  46729  sssmf  46730  issmfle  46737  issmfdmpt  46740  issmfgt  46748  issmfled  46749  issmfgtd  46753  smflimlem2  46764  smfmullem4  46786  smfpimcclem  46799  smfsuplem1  46803  smfinflem  46809  iccelpart  47428  mogoldbb  47780  sbgoldbo  47782  pgindnf  49699  aacllem  49784