Theorem ralrimi 3139

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

Syntax hints:   → wi 4  Ⅎwnf 1787   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788  df-ral 3068

This theorem is referenced by:  ralimdaa  3140  reximdai  3239  rexlimd2  3244  r19.12  3252  r19.12OLD  3253  r19.37  3270  ralcom2  3288  rabbida  3398  ralrimia  3420  2rmorex  3684  iineq2d  4944  disjxiun  5067  mpteq2daOLD  5169  rnmpt0f  6135  fnmptd  6558  mpteqb  6876  fmptdf  6973  eusvobj2  7248  offval2f  7526  zfrep6  7771  frrlem4  8076  wfrlem4OLD  8114  tfr3  8201  tz7.49  8246  mapxpen  8879  trpredmintr  9409  dfac2b  9817  hsmexlem4  10116  axcc3  10125  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  ac6num  10166  dedekind  11068  dedekindle  11069  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  fprodcllemf  15596  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  mreexexd  17274  cpmatmcllem  21775  ptcnplem  22680  xkocnv  22873  cfilucfil  23621  cncfcompt2  23977  itg2splitlem  24818  itg2split  24819  itgeq1f  24841  mptelee  27166  lfgrnloop  27398  foresf1o  30751  iinabrex  30809  funimass4f  30873  fcomptf  30897  aciunf1lem  30901  funcnvmpt  30906  fnpreimac  30910  isarchiofld  31418  reff  31691  locfinreflem  31692  zarclsiin  31723  zarcmplem  31733  prodindf  31891  esumeq12dvaf  31899  esumgsum  31913  esumel  31915  esumf1o  31918  esumc  31919  esummono  31922  gsumesum  31927  esumlub  31928  esumlef  31930  esumfsup  31938  esumpinfval  31941  esumpinfsum  31945  esum2d  31961  ldsysgenld  32028  sigapildsyslem  32029  ldgenpisyslem1  32031  measinblem  32088  voliune  32097  volmeas  32099  oms0  32164  omssubadd  32167  dstrvprob  32338  bnj1379  32710  bnj1204  32892  bnj1388  32913  bnj1417  32921  bnj1489  32936  untsucf  33551  domalom  35502  fvineqsneq  35510  cover2  35799  upixp  35814  indexdom  35819  filbcmb  35825  sdclem2  35827  eq0rabdioph  40514  eqrabdioph  40515  setindtr  40762  ss2iundf  41156  gneispace  41633  mnuprdlem3  41781  iunconnlem2  42444  rzalf  42449  fnchoice  42461  refsumcn  42462  rfcnnnub  42468  refsum2cnlem1  42469  iuneq2df  42483  uzwo4  42490  ixpeq2d  42505  ixpssmapc  42511  elintd  42513  ssdf  42514  ralimralim  42520  nelrnmpt  42523  ixpssixp  42531  ballss3  42532  iinssiin  42567  eliind2  42568  rabssd  42580  fompt  42619  choicefi  42629  iunmapss  42644  iunmapsn  42646  axccdom  42651  mptfnd  42675  ssfiunibd  42738  xralrple2  42783  infxr  42796  xrralrecnnle  42812  xrralrecnnge  42820  supxrunb3  42829  fimaxre4  42831  supxrleubrnmpt  42836  rexabslelem  42848  suprleubrnmpt  42852  uzublem  42860  infxrgelbrnmpt  42884  iooiinicc  42970  iooiinioc  42984  mccl  43029  climsuse  43039  mullimc  43047  mullimcf  43054  limcrecl  43060  limsupre  43072  limcleqr  43075  addlimc  43079  0ellimcdiv  43080  limclner  43082  limsupubuzlem  43143  climinf3  43147  limsupequzmpt2  43149  limsupmnfuzlem  43157  limsupre3uzlem  43166  liminfequzmpt2  43222  cncficcgt0  43319  cncfioobd  43328  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  dvmptfprodlem  43375  dvnprodlem1  43377  iblsplitf  43401  stoweidlem5  43436  stoweidlem16  43447  stoweidlem18  43449  stoweidlem21  43452  stoweidlem26  43457  stoweidlem27  43458  stoweidlem28  43459  stoweidlem29  43460  stoweidlem31  43462  stoweidlem34  43465  stoweidlem36  43467  stoweidlem41  43472  stoweidlem42  43473  stoweidlem44  43475  stoweidlem45  43476  stoweidlem48  43479  stoweidlem51  43482  stoweidlem55  43486  stoweidlem59  43490  stoweidlem60  43491  stoweidlem62  43493  wallispilem3  43498  stirlinglem5  43509  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem31  43569  fourierdlem39  43577  fourierdlem68  43605  fourierdlem71  43608  fourierdlem73  43610  fourierdlem77  43614  fourierdlem80  43617  fourierdlem83  43620  fourierdlem87  43624  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  etransclem32  43697  subsaliuncllem  43786  sge0revalmpt  43806  sge0fodjrnlem  43844  sge0fsummptf  43864  iundjiun  43888  meadjiun  43894  voliunsge0lem  43900  meaiininclem  43914  omeiunle  43945  hoicvrrex  43984  ovnsubaddlem2  43999  hoissrrn2  44006  hoidmv1lelem1  44019  hoidmvlelem3  44025  ovnhoilem1  44029  hoi2toco  44035  ovnlecvr2  44038  hspdifhsp  44044  hoiqssbllem1  44050  hoiqssbllem3  44052  hspmbllem2  44055  iinhoiicclem  44101  iunhoiioolem  44103  vonioo  44110  vonicc  44113  pimconstlt0  44128  pimconstlt1  44129  pimltpnf  44130  pimiooltgt  44135  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  preimageiingt  44144  preimaleiinlt  44145  issmfd  44158  issmfdf  44160  sssmf  44161  issmfle  44168  issmfdmpt  44171  issmfgt  44179  issmfled  44180  issmfgtd  44183  smflimlem2  44194  smfmullem4  44215  smfpimcclem  44227  smfsuplem1  44231  smfinflem  44237  smfinfmpt  44239  iccelpart  44773  mogoldbb  45125  sbgoldbo  45127  aacllem  46391