Theorem ralrimi 3137

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3103. (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 3103	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1791   ∈ wcel 2110  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792  df-ral 3066

This theorem is referenced by:  ralimdaa  3138  reximdai  3230  rexlimd2  3235  r19.12  3243  r19.37  3257  ralcom2  3275  rabbida  3384  ralrimia  3406  2rmorex  3667  iineq2d  4927  disjxiun  5050  mpteq2da  5149  rnmpt0f  6106  fnmptd  6519  mpteqb  6837  fmptdf  6934  eusvobj2  7206  offval2f  7483  zfrep6  7728  frrlem4  8030  wfrlem4  8058  tfr3  8135  tz7.49  8181  mapxpen  8812  trpredmintr  9336  dfac2b  9744  hsmexlem4  10043  axcc3  10052  domtriomlem  10056  axdc3lem2  10065  axdc3lem4  10067  axdc4lem  10069  ac6num  10093  dedekind  10995  dedekindle  10996  fsuppmapnn0fiublem  13563  fsuppmapnn0fiub  13564  fprodcllemf  15520  lcmfunsnlem1  16194  lcmfunsnlem2lem1  16195  lcmfunsnlem2  16197  mreexexd  17151  cpmatmcllem  21615  ptcnplem  22518  xkocnv  22711  cfilucfil  23457  cncfcompt2  23805  itg2splitlem  24646  itg2split  24647  itgeq1f  24669  mptelee  26986  lfgrnloop  27216  foresf1o  30569  iinabrex  30627  funimass4f  30691  fcomptf  30715  aciunf1lem  30719  funcnvmpt  30724  fnpreimac  30728  isarchiofld  31235  reff  31503  locfinreflem  31504  zarclsiin  31535  zarcmplem  31545  prodindf  31703  esumeq12dvaf  31711  esumgsum  31725  esumel  31727  esumf1o  31730  esumc  31731  esummono  31734  gsumesum  31739  esumlub  31740  esumlef  31742  esumfsup  31750  esumpinfval  31753  esumpinfsum  31757  esum2d  31773  ldsysgenld  31840  sigapildsyslem  31841  ldgenpisyslem1  31843  measinblem  31900  voliune  31909  volmeas  31911  oms0  31976  omssubadd  31979  dstrvprob  32150  bnj1379  32523  bnj1204  32705  bnj1388  32726  bnj1417  32734  bnj1489  32749  untsucf  33364  domalom  35312  fvineqsneq  35320  cover2  35609  upixp  35624  indexdom  35629  filbcmb  35635  sdclem2  35637  eq0rabdioph  40301  eqrabdioph  40302  setindtr  40549  ss2iundf  40944  gneispace  41421  mnuprdlem3  41565  iunconnlem2  42228  rzalf  42233  fnchoice  42245  refsumcn  42246  rfcnnnub  42252  refsum2cnlem1  42253  iuneq2df  42267  uzwo4  42274  ixpeq2d  42289  ixpssmapc  42295  elintd  42297  ssdf  42298  ralimralim  42304  nelrnmpt  42307  ixpssixp  42315  ballss3  42316  iinssiin  42351  eliind2  42352  rabssd  42364  fompt  42403  choicefi  42413  iunmapss  42428  iunmapsn  42430  axccdom  42435  mptfnd  42458  ssfiunibd  42521  xralrple2  42566  infxr  42579  xrralrecnnle  42595  xrralrecnnge  42603  supxrunb3  42612  fimaxre4  42614  supxrleubrnmpt  42619  rexabslelem  42631  suprleubrnmpt  42635  uzublem  42643  infxrgelbrnmpt  42669  iooiinicc  42755  iooiinioc  42769  mccl  42814  climsuse  42824  mullimc  42832  mullimcf  42839  limcrecl  42845  limsupre  42857  limcleqr  42860  addlimc  42864  0ellimcdiv  42865  limclner  42867  limsupubuzlem  42928  climinf3  42932  limsupequzmpt2  42934  limsupmnfuzlem  42942  limsupre3uzlem  42951  liminfequzmpt2  43007  cncficcgt0  43104  cncfioobd  43113  fprodsubrecnncnvlem  43123  fprodaddrecnncnvlem  43125  dvmptfprodlem  43160  dvnprodlem1  43162  iblsplitf  43186  stoweidlem5  43221  stoweidlem16  43232  stoweidlem18  43234  stoweidlem21  43237  stoweidlem26  43242  stoweidlem27  43243  stoweidlem28  43244  stoweidlem29  43245  stoweidlem31  43247  stoweidlem34  43250  stoweidlem36  43252  stoweidlem41  43257  stoweidlem42  43258  stoweidlem44  43260  stoweidlem45  43261  stoweidlem48  43264  stoweidlem51  43267  stoweidlem55  43271  stoweidlem59  43275  stoweidlem60  43276  stoweidlem62  43278  wallispilem3  43283  stirlinglem5  43294  fourierdlem16  43339  fourierdlem21  43344  fourierdlem22  43345  fourierdlem31  43354  fourierdlem39  43362  fourierdlem68  43390  fourierdlem71  43393  fourierdlem73  43395  fourierdlem77  43399  fourierdlem80  43402  fourierdlem83  43405  fourierdlem87  43409  fourierdlem94  43416  fourierdlem103  43425  fourierdlem104  43426  fourierdlem112  43434  fourierdlem113  43435  etransclem32  43482  subsaliuncllem  43571  sge0revalmpt  43591  sge0fodjrnlem  43629  sge0fsummptf  43649  iundjiun  43673  meadjiun  43679  voliunsge0lem  43685  meaiininclem  43699  omeiunle  43730  hoicvrrex  43769  ovnsubaddlem2  43784  hoissrrn2  43791  hoidmv1lelem1  43804  hoidmvlelem3  43810  ovnhoilem1  43814  hoi2toco  43820  ovnlecvr2  43823  hspdifhsp  43829  hoiqssbllem1  43835  hoiqssbllem3  43837  hspmbllem2  43840  iinhoiicclem  43886  iunhoiioolem  43888  vonioo  43895  vonicc  43898  pimconstlt0  43913  pimconstlt1  43914  pimltpnf  43915  pimiooltgt  43920  pimdecfgtioc  43924  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  preimageiingt  43929  preimaleiinlt  43930  issmfd  43943  issmfdf  43945  sssmf  43946  issmfle  43953  issmfdmpt  43956  issmfgt  43964  issmfled  43965  issmfgtd  43968  smflimlem2  43979  smfmullem4  44000  smfpimcclem  44012  smfsuplem1  44016  smfsupmpt  44020  smfinflem  44022  smfinfmpt  44024  iccelpart  44558  mogoldbb  44910  sbgoldbo  44912  aacllem  46176