Theorem ralrimi 3216

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785  df-ral 3143

This theorem is referenced by:  ralimdaa  3217  reximdai  3311  rexlimd2  3316  r19.12  3324  r19.12OLD  3327  r19.37  3343  ralcom2  3363  rabbida  3474  2rmorex  3745  iineq2d  4942  disjxiun  5063  mpteq2da  5160  fnmptd  6489  mpteqb  6787  fmptdf  6881  eusvobj2  7149  offval2f  7421  zfrep6  7656  wfrlem4  7958  tfr3  8035  tz7.49  8081  mapxpen  8683  dfac2b  9556  hsmexlem4  9851  axcc3  9860  domtriomlem  9864  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  ac6num  9901  dedekind  10803  dedekindle  10804  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  fprodcllemf  15312  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem2  15984  mreexexd  16919  cpmatmcllem  21326  ptcnplem  22229  xkocnv  22422  cfilucfil  23169  itg2splitlem  24349  itg2split  24350  itgeq1f  24372  mptelee  26681  lfgrnloop  26910  foresf1o  30265  funimass4f  30382  fcomptf  30403  aciunf1lem  30407  funcnvmpt  30412  fnpreimac  30416  isarchiofld  30890  reff  31103  locfinreflem  31104  prodindf  31282  esumeq12dvaf  31290  esumgsum  31304  esumel  31306  esumf1o  31309  esumc  31310  esummono  31313  gsumesum  31318  esumlub  31319  esumlef  31321  esumfsup  31329  esumpinfval  31332  esumpinfsum  31336  esum2d  31352  ldsysgenld  31419  sigapildsyslem  31420  ldgenpisyslem1  31422  measinblem  31479  voliune  31488  volmeas  31490  oms0  31555  omssubadd  31558  dstrvprob  31729  bnj1379  32102  bnj1204  32284  bnj1388  32305  bnj1417  32313  bnj1489  32328  untsucf  32936  trpredmintr  33070  frrlem4  33126  domalom  34688  fvineqsneq  34696  cover2  35004  upixp  35019  indexdom  35024  filbcmb  35030  sdclem2  35032  eq0rabdioph  39422  eqrabdioph  39423  setindtr  39670  ss2iundf  40053  gneispace  40533  mnuprdlem3  40659  iunconnlem2  41318  rzalf  41323  fnchoice  41335  refsumcn  41336  rfcnnnub  41342  refsum2cnlem1  41343  iuneq2df  41357  uzwo4  41364  ixpeq2d  41379  ixpssmapc  41385  elintd  41387  ssdf  41388  ralimralim  41394  nelrnmpt  41397  ixpssixp  41407  ballss3  41408  iinssiin  41444  eliind2  41445  ralrimia  41447  rabssd  41460  fompt  41502  choicefi  41512  iunmapss  41527  iunmapsn  41529  axccdom  41536  mptfnd  41561  ssfiunibd  41625  xralrple2  41671  infxr  41684  xrralrecnnle  41702  xrralrecnnge  41711  supxrunb3  41721  fimaxre4  41723  supxrleubrnmpt  41728  rexabslelem  41741  suprleubrnmpt  41745  uzublem  41753  infxrgelbrnmpt  41779  iooiinicc  41867  iooiinioc  41881  mccl  41928  climsuse  41938  mullimc  41946  mullimcf  41953  limcrecl  41959  limsupre  41971  limcleqr  41974  addlimc  41978  0ellimcdiv  41979  limclner  41981  limsupubuzlem  42042  climinf3  42046  limsupequzmpt2  42048  limsupmnfuzlem  42056  limsupre3uzlem  42065  liminfequzmpt2  42121  cncficcgt0  42220  cncfioobd  42229  cncfcompt2  42231  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  dvmptfprodlem  42278  dvnprodlem1  42280  iblsplitf  42304  stoweidlem5  42339  stoweidlem16  42350  stoweidlem18  42352  stoweidlem21  42355  stoweidlem26  42360  stoweidlem27  42361  stoweidlem28  42362  stoweidlem29  42363  stoweidlem31  42365  stoweidlem34  42368  stoweidlem36  42370  stoweidlem41  42375  stoweidlem42  42376  stoweidlem44  42378  stoweidlem45  42379  stoweidlem48  42382  stoweidlem51  42385  stoweidlem55  42389  stoweidlem59  42393  stoweidlem60  42394  stoweidlem62  42396  wallispilem3  42401  stirlinglem5  42412  fourierdlem16  42457  fourierdlem21  42462  fourierdlem22  42463  fourierdlem31  42472  fourierdlem39  42480  fourierdlem68  42508  fourierdlem71  42511  fourierdlem73  42513  fourierdlem77  42517  fourierdlem80  42520  fourierdlem83  42523  fourierdlem87  42527  fourierdlem94  42534  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  fourierdlem113  42553  etransclem32  42600  subsaliuncllem  42689  sge0revalmpt  42709  sge0fodjrnlem  42747  sge0fsummptf  42767  iundjiun  42791  meadjiun  42797  voliunsge0lem  42803  meaiininclem  42817  omeiunle  42848  hoicvrrex  42887  ovnsubaddlem2  42902  hoissrrn2  42909  hoidmv1lelem1  42922  hoidmvlelem3  42928  ovnhoilem1  42932  hoi2toco  42938  ovnlecvr2  42941  hspdifhsp  42947  hoiqssbllem1  42953  hoiqssbllem3  42955  hspmbllem2  42958  iinhoiicclem  43004  iunhoiioolem  43006  vonioo  43013  vonicc  43016  pimconstlt0  43031  pimconstlt1  43032  pimltpnf  43033  pimiooltgt  43038  pimdecfgtioc  43042  pimincfltioc  43043  pimdecfgtioo  43044  pimincfltioo  43045  preimageiingt  43047  preimaleiinlt  43048  issmfd  43061  issmfdf  43063  sssmf  43064  issmfle  43071  issmfdmpt  43074  issmfgt  43082  issmfled  43083  issmfgtd  43086  smflimlem2  43097  smfmullem4  43118  smfpimcclem  43130  smfsuplem1  43134  smfsupmpt  43138  smfinflem  43140  smfinfmpt  43142  iccelpart  43642  mogoldbb  43999  sbgoldbo  44001  aacllem  44951