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 3128. (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3127. (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 2203	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		ralrimi.2	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	2, 3	hbralrimi 3127	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786  df-ral 3053

This theorem is referenced by:  ralrimia  3236  ralimdaa  3238  reximdai  3239  r19.37  3240  rexlimd2  3243  r19.12  3286  ralcom2  3348  rabbidaOLD  3438  2rmorex  3713  iineq2d  4971  disjxiun  5096  nelrnmpt  5917  rnmpt0f  6202  fnmptd  6634  mpteqb  6962  fmptdf  7064  eusvobj2  7352  offval2f  7639  zfrep6  7901  frrlem4  8233  tfr3  8332  tz7.49  8378  mapxpen  9075  dfac2b  10045  hsmexlem4  10343  axcc3  10352  domtriomlem  10356  axdc3lem2  10365  axdc3lem4  10367  axdc4lem  10369  ac6num  10393  dedekind  11300  dedekindle  11301  fsuppmapnn0fiublem  13917  fsuppmapnn0fiub  13918  fprodcllemf  15885  lcmfunsnlem1  16568  lcmfunsnlem2lem1  16569  lcmfunsnlem2  16571  mreexexd  17575  cpmatmcllem  22666  ptcnplem  23569  xkocnv  23762  cfilucfil  24507  cncfcompt2  24861  itg2splitlem  25709  itg2split  25710  itgeq1fOLD  25733  bdaypw2n0bndlem  28463  mpteleeOLD  28972  lfgrnloop  29202  foresf1o  32582  iinabrex  32647  funimass4f  32718  fcomptf  32739  aciunf1lem  32743  fnpreimac  32751  prodindf  32946  isarchiofld  33283  reff  33998  locfinreflem  33999  zarclsiin  34030  zarcmplem  34040  esumeq12dvaf  34190  esumgsum  34204  esumel  34206  esumf1o  34209  esumc  34210  esummono  34213  gsumesum  34218  esumlub  34219  esumlef  34221  esumfsup  34229  esumpinfval  34232  esumpinfsum  34236  esum2d  34252  ldsysgenld  34319  sigapildsyslem  34320  ldgenpisyslem1  34322  measinblem  34379  voliune  34388  volmeas  34390  oms0  34456  omssubadd  34459  dstrvprob  34631  bnj1379  34988  bnj1204  35170  bnj1388  35191  bnj1417  35199  bnj1489  35214  untsucf  35906  domalom  37611  fvineqsneq  37619  cover2  37918  upixp  37932  indexdom  37937  filbcmb  37943  sdclem2  37945  eq0rabdioph  43085  eqrabdioph  43086  setindtr  43333  gneispace  44442  mnuprdlem3  44582  iunconnlem2  45242  rzalf  45329  fnchoice  45341  refsumcn  45342  rfcnnnub  45348  refsum2cnlem1  45349  iuneq2df  45359  uzwo4  45365  ixpeq2d  45380  ixpssmapc  45385  elintd  45386  ssdf  45387  ralimralim  45393  ixpssixp  45403  ballss3  45404  iinssiin  45440  eliind2  45441  rabssd  45453  choicefi  45511  iunmapss  45526  iunmapsn  45528  axccdom  45533  mptfnd  45553  ssfiunibd  45624  xralrple2  45666  infxr  45678  xrralrecnnle  45694  xrralrecnnge  45701  supxrunb3  45710  fimaxre4  45712  supxrleubrnmpt  45717  rexabslelem  45729  suprleubrnmpt  45733  uzublem  45741  infxrgelbrnmpt  45765  iooiinicc  45855  iooiinioc  45869  mccl  45911  climsuse  45921  mullimc  45929  mullimcf  45936  limcrecl  45942  limsupre  45952  limcleqr  45955  addlimc  45959  0ellimcdiv  45960  limclner  45962  limsupubuzlem  46023  climinf3  46027  limsupequzmpt2  46029  limsupmnfuzlem  46037  limsupre3uzlem  46046  liminfequzmpt2  46102  cncficcgt0  46199  cncfioobd  46208  fprodsubrecnncnvlem  46218  fprodaddrecnncnvlem  46220  dvmptfprodlem  46255  dvnprodlem1  46257  iblsplitf  46281  stoweidlem5  46316  stoweidlem16  46327  stoweidlem18  46329  stoweidlem21  46332  stoweidlem26  46337  stoweidlem27  46338  stoweidlem28  46339  stoweidlem29  46340  stoweidlem31  46342  stoweidlem34  46345  stoweidlem36  46347  stoweidlem41  46352  stoweidlem42  46353  stoweidlem44  46355  stoweidlem45  46356  stoweidlem48  46359  stoweidlem51  46362  stoweidlem55  46366  stoweidlem59  46370  stoweidlem60  46371  stoweidlem62  46373  wallispilem3  46378  stirlinglem5  46389  fourierdlem16  46434  fourierdlem21  46439  fourierdlem22  46440  fourierdlem31  46449  fourierdlem39  46457  fourierdlem68  46485  fourierdlem71  46488  fourierdlem73  46490  fourierdlem77  46494  fourierdlem80  46497  fourierdlem83  46500  fourierdlem87  46504  fourierdlem94  46511  fourierdlem103  46520  fourierdlem104  46521  fourierdlem112  46529  fourierdlem113  46530  etransclem32  46577  subsaliuncllem  46668  sge0revalmpt  46689  sge0fodjrnlem  46727  sge0fsummptf  46747  iundjiun  46771  meadjiun  46777  voliunsge0lem  46783  meaiininclem  46797  omeiunle  46828  hoicvrrex  46867  ovnsubaddlem2  46882  hoissrrn2  46889  hoidmv1lelem1  46902  hoidmvlelem3  46908  ovnhoilem1  46912  hoi2toco  46918  ovnlecvr2  46921  hspdifhsp  46927  hoiqssbllem1  46933  hoiqssbllem3  46935  hspmbllem2  46938  iinhoiicclem  46984  iunhoiioolem  46986  vonioo  46993  vonicc  46996  pimconstlt0  47012  pimconstlt1  47013  pimltpnff  47014  pimiooltgt  47021  pimdecfgtioc  47026  pimincfltioc  47027  pimdecfgtioo  47028  pimincfltioo  47029  pimgtmnff  47033  issmfd  47046  issmfdf  47048  sssmf  47049  issmfle  47056  issmfdmpt  47059  issmfgt  47067  issmfled  47068  issmfgtd  47072  smflimlem2  47083  smfmullem4  47105  smfpimcclem  47118  smfsuplem1  47122  smfinflem  47128  iccelpart  47746  mogoldbb  48098  sbgoldbo  48100  pgindnf  50028  aacllem  50113