Theorem ralrimi 3255

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

Syntax hints:   → wi 4  Ⅎwnf 1780   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781  df-ral 3060

This theorem is referenced by:  ralrimia  3256  ralimdaa  3258  reximdai  3259  r19.37  3260  rexlimd2  3263  r19.12  3312  r19.12OLD  3313  ralcom2  3375  rabbidaOLD  3475  2rmorex  3763  iineq2d  5020  disjxiun  5145  mpteq2daOLD  5247  rnmpt0f  6265  fnmptd  6710  mpteqb  7035  fmptdf  7137  eusvobj2  7423  offval2f  7712  zfrep6  7978  frrlem4  8313  wfrlem4OLD  8351  tfr3  8438  tz7.49  8484  mapxpen  9182  dfac2b  10169  hsmexlem4  10467  axcc3  10476  domtriomlem  10480  axdc3lem2  10489  axdc3lem4  10491  axdc4lem  10493  ac6num  10517  dedekind  11422  dedekindle  11423  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  fprodcllemf  15991  lcmfunsnlem1  16671  lcmfunsnlem2lem1  16672  lcmfunsnlem2  16674  mreexexd  17693  cpmatmcllem  22740  ptcnplem  23645  xkocnv  23838  cfilucfil  24588  cncfcompt2  24948  itg2splitlem  25798  itg2split  25799  itgeq1fOLD  25822  mptelee  28925  lfgrnloop  29157  foresf1o  32532  iinabrex  32589  funimass4f  32654  fcomptf  32675  aciunf1lem  32679  funcnvmpt  32684  fnpreimac  32688  isarchiofld  33327  reff  33800  locfinreflem  33801  zarclsiin  33832  zarcmplem  33842  prodindf  34004  esumeq12dvaf  34012  esumgsum  34026  esumel  34028  esumf1o  34031  esumc  34032  esummono  34035  gsumesum  34040  esumlub  34041  esumlef  34043  esumfsup  34051  esumpinfval  34054  esumpinfsum  34058  esum2d  34074  ldsysgenld  34141  sigapildsyslem  34142  ldgenpisyslem1  34144  measinblem  34201  voliune  34210  volmeas  34212  oms0  34279  omssubadd  34282  dstrvprob  34453  bnj1379  34823  bnj1204  35005  bnj1388  35026  bnj1417  35034  bnj1489  35049  untsucf  35690  domalom  37387  fvineqsneq  37395  cover2  37702  upixp  37716  indexdom  37721  filbcmb  37727  sdclem2  37729  eq0rabdioph  42764  eqrabdioph  42765  setindtr  43013  gneispace  44124  mnuprdlem3  44270  iunconnlem2  44933  rzalf  44955  fnchoice  44967  refsumcn  44968  rfcnnnub  44974  refsum2cnlem1  44975  iuneq2df  44986  uzwo4  44993  ixpeq2d  45008  ixpssmapc  45013  elintd  45014  ssdf  45015  ralimralim  45021  nelrnmpt  45024  ixpssixp  45032  ballss3  45033  iinssiin  45069  eliind2  45070  rabssd  45082  ss2rabdf  45093  choicefi  45143  iunmapss  45158  iunmapsn  45160  axccdom  45165  mptfnd  45186  ssfiunibd  45260  xralrple2  45304  infxr  45317  xrralrecnnle  45333  xrralrecnnge  45340  supxrunb3  45349  fimaxre4  45351  supxrleubrnmpt  45356  rexabslelem  45368  suprleubrnmpt  45372  uzublem  45380  infxrgelbrnmpt  45404  iooiinicc  45495  iooiinioc  45509  mccl  45554  climsuse  45564  mullimc  45572  mullimcf  45579  limcrecl  45585  limsupre  45597  limcleqr  45600  addlimc  45604  0ellimcdiv  45605  limclner  45607  limsupubuzlem  45668  climinf3  45672  limsupequzmpt2  45674  limsupmnfuzlem  45682  limsupre3uzlem  45691  liminfequzmpt2  45747  cncficcgt0  45844  cncfioobd  45853  fprodsubrecnncnvlem  45863  fprodaddrecnncnvlem  45865  dvmptfprodlem  45900  dvnprodlem1  45902  iblsplitf  45926  stoweidlem5  45961  stoweidlem16  45972  stoweidlem18  45974  stoweidlem21  45977  stoweidlem26  45982  stoweidlem27  45983  stoweidlem28  45984  stoweidlem29  45985  stoweidlem31  45987  stoweidlem34  45990  stoweidlem36  45992  stoweidlem41  45997  stoweidlem42  45998  stoweidlem44  46000  stoweidlem45  46001  stoweidlem48  46004  stoweidlem51  46007  stoweidlem55  46011  stoweidlem59  46015  stoweidlem60  46016  stoweidlem62  46018  wallispilem3  46023  stirlinglem5  46034  fourierdlem16  46079  fourierdlem21  46084  fourierdlem22  46085  fourierdlem31  46094  fourierdlem39  46102  fourierdlem68  46130  fourierdlem71  46133  fourierdlem73  46135  fourierdlem77  46139  fourierdlem80  46142  fourierdlem83  46145  fourierdlem87  46149  fourierdlem94  46156  fourierdlem103  46165  fourierdlem104  46166  fourierdlem112  46174  fourierdlem113  46175  etransclem32  46222  subsaliuncllem  46313  sge0revalmpt  46334  sge0fodjrnlem  46372  sge0fsummptf  46392  iundjiun  46416  meadjiun  46422  voliunsge0lem  46428  meaiininclem  46442  omeiunle  46473  hoicvrrex  46512  ovnsubaddlem2  46527  hoissrrn2  46534  hoidmv1lelem1  46547  hoidmvlelem3  46553  ovnhoilem1  46557  hoi2toco  46563  ovnlecvr2  46566  hspdifhsp  46572  hoiqssbllem1  46578  hoiqssbllem3  46580  hspmbllem2  46583  iinhoiicclem  46629  iunhoiioolem  46631  vonioo  46638  vonicc  46641  pimconstlt0  46657  pimconstlt1  46658  pimltpnff  46659  pimiooltgt  46666  pimdecfgtioc  46671  pimincfltioc  46672  pimdecfgtioo  46673  pimincfltioo  46674  preimageiingt  46676  preimaleiinlt  46677  pimgtmnff  46678  issmfd  46691  issmfdf  46693  sssmf  46694  issmfle  46701  issmfdmpt  46704  issmfgt  46712  issmfled  46713  issmfgtd  46717  smflimlem2  46728  smfmullem4  46750  smfpimcclem  46763  smfsuplem1  46767  smfinflem  46773  iccelpart  47358  mogoldbb  47710  sbgoldbo  47712  pgindnf  48947  aacllem  49032