Theorem ralrimi 3254

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2106  ∀wral 3061

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786  df-ral 3062

This theorem is referenced by:  ralrimia  3255  ralimdaa  3257  reximdai  3258  r19.37  3259  rexlimd2  3262  r19.12  3311  r19.12OLD  3312  ralcom2  3373  rabbidaOLD  3470  2rmorex  3749  iineq2d  5019  disjxiun  5144  mpteq2daOLD  5246  rnmpt0f  6239  fnmptd  6688  mpteqb  7014  fmptdf  7113  eusvobj2  7397  offval2f  7681  zfrep6  7937  frrlem4  8270  wfrlem4OLD  8308  tfr3  8395  tz7.49  8441  mapxpen  9139  dfac2b  10121  hsmexlem4  10420  axcc3  10429  domtriomlem  10433  axdc3lem2  10442  axdc3lem4  10444  axdc4lem  10446  ac6num  10470  dedekind  11373  dedekindle  11374  fsuppmapnn0fiublem  13951  fsuppmapnn0fiub  13952  fprodcllemf  15898  lcmfunsnlem1  16570  lcmfunsnlem2lem1  16571  lcmfunsnlem2  16573  mreexexd  17588  cpmatmcllem  22211  ptcnplem  23116  xkocnv  23309  cfilucfil  24059  cncfcompt2  24415  itg2splitlem  25257  itg2split  25258  itgeq1f  25280  mptelee  28142  lfgrnloop  28374  foresf1o  31729  iinabrex  31787  funimass4f  31848  fcomptf  31870  aciunf1lem  31874  funcnvmpt  31879  fnpreimac  31883  isarchiofld  32423  reff  32807  locfinreflem  32808  zarclsiin  32839  zarcmplem  32849  prodindf  33009  esumeq12dvaf  33017  esumgsum  33031  esumel  33033  esumf1o  33036  esumc  33037  esummono  33040  gsumesum  33045  esumlub  33046  esumlef  33048  esumfsup  33056  esumpinfval  33059  esumpinfsum  33063  esum2d  33079  ldsysgenld  33146  sigapildsyslem  33147  ldgenpisyslem1  33149  measinblem  33206  voliune  33215  volmeas  33217  oms0  33284  omssubadd  33287  dstrvprob  33458  bnj1379  33829  bnj1204  34011  bnj1388  34032  bnj1417  34040  bnj1489  34055  untsucf  34667  domalom  36273  fvineqsneq  36281  cover2  36571  upixp  36585  indexdom  36590  filbcmb  36596  sdclem2  36598  eq0rabdioph  41499  eqrabdioph  41500  setindtr  41748  gneispace  42870  mnuprdlem3  43018  iunconnlem2  43681  rzalf  43686  fnchoice  43698  refsumcn  43699  rfcnnnub  43705  refsum2cnlem1  43706  iuneq2df  43718  uzwo4  43725  ixpeq2d  43740  ixpssmapc  43746  elintd  43748  ssdf  43749  ralimralim  43755  nelrnmpt  43758  ixpssixp  43766  ballss3  43767  iinssiin  43803  eliind2  43804  rabssd  43816  ss2rabdf  43829  fompt  43875  choicefi  43884  iunmapss  43899  iunmapsn  43901  axccdom  43906  mptfnd  43930  ssfiunibd  44005  xralrple2  44050  infxr  44063  xrralrecnnle  44079  xrralrecnnge  44086  supxrunb3  44095  fimaxre4  44097  supxrleubrnmpt  44102  rexabslelem  44114  suprleubrnmpt  44118  uzublem  44126  infxrgelbrnmpt  44150  iooiinicc  44241  iooiinioc  44255  mccl  44300  climsuse  44310  mullimc  44318  mullimcf  44325  limcrecl  44331  limsupre  44343  limcleqr  44346  addlimc  44350  0ellimcdiv  44351  limclner  44353  limsupubuzlem  44414  climinf3  44418  limsupequzmpt2  44420  limsupmnfuzlem  44428  limsupre3uzlem  44437  liminfequzmpt2  44493  cncficcgt0  44590  cncfioobd  44599  fprodsubrecnncnvlem  44609  fprodaddrecnncnvlem  44611  dvmptfprodlem  44646  dvnprodlem1  44648  iblsplitf  44672  stoweidlem5  44707  stoweidlem16  44718  stoweidlem18  44720  stoweidlem21  44723  stoweidlem26  44728  stoweidlem27  44729  stoweidlem28  44730  stoweidlem29  44731  stoweidlem31  44733  stoweidlem34  44736  stoweidlem36  44738  stoweidlem41  44743  stoweidlem42  44744  stoweidlem44  44746  stoweidlem45  44747  stoweidlem48  44750  stoweidlem51  44753  stoweidlem55  44757  stoweidlem59  44761  stoweidlem60  44762  stoweidlem62  44764  wallispilem3  44769  stirlinglem5  44780  fourierdlem16  44825  fourierdlem21  44830  fourierdlem22  44831  fourierdlem31  44840  fourierdlem39  44848  fourierdlem68  44876  fourierdlem71  44879  fourierdlem73  44881  fourierdlem77  44885  fourierdlem80  44888  fourierdlem83  44891  fourierdlem87  44895  fourierdlem94  44902  fourierdlem103  44911  fourierdlem104  44912  fourierdlem112  44920  fourierdlem113  44921  etransclem32  44968  subsaliuncllem  45059  sge0revalmpt  45080  sge0fodjrnlem  45118  sge0fsummptf  45138  iundjiun  45162  meadjiun  45168  voliunsge0lem  45174  meaiininclem  45188  omeiunle  45219  hoicvrrex  45258  ovnsubaddlem2  45273  hoissrrn2  45280  hoidmv1lelem1  45293  hoidmvlelem3  45299  ovnhoilem1  45303  hoi2toco  45309  ovnlecvr2  45312  hspdifhsp  45318  hoiqssbllem1  45324  hoiqssbllem3  45326  hspmbllem2  45329  iinhoiicclem  45375  iunhoiioolem  45377  vonioo  45384  vonicc  45387  pimconstlt0  45403  pimconstlt1  45404  pimltpnff  45405  pimiooltgt  45412  pimdecfgtioc  45417  pimincfltioc  45418  pimdecfgtioo  45419  pimincfltioo  45420  preimageiingt  45422  preimaleiinlt  45423  pimgtmnff  45424  issmfd  45437  issmfdf  45439  sssmf  45440  issmfle  45447  issmfdmpt  45450  issmfgt  45458  issmfled  45459  issmfgtd  45463  smflimlem2  45474  smfmullem4  45496  smfpimcclem  45509  smfsuplem1  45513  smfinflem  45519  smfinfmpt  45521  iccelpart  46087  mogoldbb  46439  sbgoldbo  46441  pgindnf  47714  aacllem  47801