Theorem ralrimi 3180

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786  df-ral 3111

This theorem is referenced by:  ralimdaa  3181  reximdai  3270  rexlimd2  3275  r19.12  3283  r19.37  3297  ralcom2  3316  rabbida  3421  2rmorex  3693  iineq2d  4904  disjxiun  5027  mpteq2da  5124  fnmptd  6461  mpteqb  6764  fmptdf  6858  eusvobj2  7128  offval2f  7401  zfrep6  7638  wfrlem4  7941  tfr3  8018  tz7.49  8064  mapxpen  8667  dfac2b  9541  hsmexlem4  9840  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  ac6num  9890  dedekind  10792  dedekindle  10793  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  fprodcllemf  15304  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  mreexexd  16911  cpmatmcllem  21323  ptcnplem  22226  xkocnv  22419  cfilucfil  23166  cncfcompt2  23513  itg2splitlem  24352  itg2split  24353  itgeq1f  24375  mptelee  26689  lfgrnloop  26918  foresf1o  30273  iinabrex  30332  funimass4f  30396  fcomptf  30421  aciunf1lem  30425  funcnvmpt  30430  fnpreimac  30434  isarchiofld  30941  reff  31192  locfinreflem  31193  zarclsiin  31224  zarcmplem  31234  prodindf  31392  esumeq12dvaf  31400  esumgsum  31414  esumel  31416  esumf1o  31419  esumc  31420  esummono  31423  gsumesum  31428  esumlub  31429  esumlef  31431  esumfsup  31439  esumpinfval  31442  esumpinfsum  31446  esum2d  31462  ldsysgenld  31529  sigapildsyslem  31530  ldgenpisyslem1  31532  measinblem  31589  voliune  31598  volmeas  31600  oms0  31665  omssubadd  31668  dstrvprob  31839  bnj1379  32212  bnj1204  32394  bnj1388  32415  bnj1417  32423  bnj1489  32438  untsucf  33049  trpredmintr  33183  frrlem4  33239  domalom  34821  fvineqsneq  34829  cover2  35152  upixp  35167  indexdom  35172  filbcmb  35178  sdclem2  35180  eq0rabdioph  39717  eqrabdioph  39718  setindtr  39965  ss2iundf  40360  gneispace  40837  mnuprdlem3  40982  iunconnlem2  41641  rzalf  41646  fnchoice  41658  refsumcn  41659  rfcnnnub  41665  refsum2cnlem1  41666  iuneq2df  41680  uzwo4  41687  ixpeq2d  41702  ixpssmapc  41708  elintd  41710  ssdf  41711  ralimralim  41717  nelrnmpt  41720  ixpssixp  41728  ballss3  41729  iinssiin  41764  eliind2  41765  ralrimia  41767  rabssd  41779  fompt  41819  choicefi  41829  iunmapss  41844  iunmapsn  41846  axccdom  41853  mptfnd  41878  ssfiunibd  41941  xralrple2  41986  infxr  41999  xrralrecnnle  42017  xrralrecnnge  42026  supxrunb3  42036  fimaxre4  42038  supxrleubrnmpt  42043  rexabslelem  42055  suprleubrnmpt  42059  uzublem  42067  infxrgelbrnmpt  42093  iooiinicc  42179  iooiinioc  42193  mccl  42240  climsuse  42250  mullimc  42258  mullimcf  42265  limcrecl  42271  limsupre  42283  limcleqr  42286  addlimc  42290  0ellimcdiv  42291  limclner  42293  limsupubuzlem  42354  climinf3  42358  limsupequzmpt2  42360  limsupmnfuzlem  42368  limsupre3uzlem  42377  liminfequzmpt2  42433  cncficcgt0  42530  cncfioobd  42539  fprodsubrecnncnvlem  42549  fprodaddrecnncnvlem  42551  dvmptfprodlem  42586  dvnprodlem1  42588  iblsplitf  42612  stoweidlem5  42647  stoweidlem16  42658  stoweidlem18  42660  stoweidlem21  42663  stoweidlem26  42668  stoweidlem27  42669  stoweidlem28  42670  stoweidlem29  42671  stoweidlem31  42673  stoweidlem34  42676  stoweidlem36  42678  stoweidlem41  42683  stoweidlem42  42684  stoweidlem44  42686  stoweidlem45  42687  stoweidlem48  42690  stoweidlem51  42693  stoweidlem55  42697  stoweidlem59  42701  stoweidlem60  42702  stoweidlem62  42704  wallispilem3  42709  stirlinglem5  42720  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem31  42780  fourierdlem39  42788  fourierdlem68  42816  fourierdlem71  42819  fourierdlem73  42821  fourierdlem77  42825  fourierdlem80  42828  fourierdlem83  42831  fourierdlem87  42835  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem113  42861  etransclem32  42908  subsaliuncllem  42997  sge0revalmpt  43017  sge0fodjrnlem  43055  sge0fsummptf  43075  iundjiun  43099  meadjiun  43105  voliunsge0lem  43111  meaiininclem  43125  omeiunle  43156  hoicvrrex  43195  ovnsubaddlem2  43210  hoissrrn2  43217  hoidmv1lelem1  43230  hoidmvlelem3  43236  ovnhoilem1  43240  hoi2toco  43246  ovnlecvr2  43249  hspdifhsp  43255  hoiqssbllem1  43261  hoiqssbllem3  43263  hspmbllem2  43266  iinhoiicclem  43312  iunhoiioolem  43314  vonioo  43321  vonicc  43324  pimconstlt0  43339  pimconstlt1  43340  pimltpnf  43341  pimiooltgt  43346  pimdecfgtioc  43350  pimincfltioc  43351  pimdecfgtioo  43352  pimincfltioo  43353  preimageiingt  43355  preimaleiinlt  43356  issmfd  43369  issmfdf  43371  sssmf  43372  issmfle  43379  issmfdmpt  43382  issmfgt  43390  issmfled  43391  issmfgtd  43394  smflimlem2  43405  smfmullem4  43426  smfpimcclem  43438  smfsuplem1  43442  smfsupmpt  43446  smfinflem  43448  smfinfmpt  43450  iccelpart  43950  mogoldbb  44303  sbgoldbo  44305  aacllem  45329