Theorem ralrimi 3260

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817  df-ral 3077

This theorem is used by:  ralrimia  3261  reximdai  3264  r19.37  3265  rexlimd2  3268  r19.12  3311  ralcom2  3362  2rmorex  3711  disjxiun  5099  nelrnmpt  5945  rnmpt0f  6233  fnmptd  6668  mpteqb  7001  fmptdf  7105  eusvobj2  7400  offval2f  7691  zfrep6OLD  7950  frrlem4  8285  tfr3  8385  tz7.49  8433  mapxpen  9140  dfac2b  10180  hsmexlem4  10478  axcc3  10487  domtriomlem  10491  axdc3lem2  10500  axdc3lem4  10502  axdc4lem  10504  ac6num  10528  dedekind  11444  dedekindle  11445  fsuppmapnn0fiublem  14101  fsuppmapnn0fiub  14102  fprodcllemf  16092  lcmfunsnlem1  16774  lcmfunsnlem2lem1  16775  lcmfunsnlem2  16777  mreexexd  17783  cpmatmcllem  22997  ptcnplem  23901  xkocnv  24094  cfilucfil  24839  cncfcompt2  25190  itg2splitlem  26030  itg2split  26031  bdaypw2n0bndlem  28782  mpteleeOLD  29406  lfgrnloop  29636  foresf1o  33033  iinabrex  33096  funimass4f  33164  fcomptf  33185  aciunf1lem  33189  fnpreimac  33197  prodindf  33362  isarchiofld  33693  reff  34404  locfinreflem  34405  zarclsiin  34436  zarcmplem  34446  esumeq12dvaf  34596  esumgsum  34610  esumel  34612  esumf1o  34615  esumc  34616  esummono  34619  gsumesum  34624  esumlub  34625  esumlef  34627  esumfsup  34635  esumpinfval  34638  esumpinfsum  34642  esum2d  34658  ldsysgenld  34726  sigapildsyslem  34727  ldgenpisyslem1  34729  measinblem  34786  voliune  34795  volmeas  34797  oms0  34863  omssubadd  34866  dstrvprob  35038  bnj1379  35394  bnj1204  35576  bnj1388  35597  bnj1417  35605  bnj1489  35620  untsucf  36396  domalom  38247  fvineqsneq  38255  cover2  38569  upixp  38583  indexdom  38588  filbcmb  38594  sdclem2  38596  eq0rabdioph  43725  eqrabdioph  43726  setindtr  43969  gneispace  45078  mnuprdlem3  45202  iunconnlem2  45861  rzalf  45955  fnchoice  45967  refsumcn  45968  rfcnnnub  45974  refsum2cnlem1  45975  iuneq2df  45985  uzwo4  45991  ixpeq2d  46006  ixpssmapc  46011  elintd  46012  ssdf  46013  ralimralim  46019  ixpssixp  46028  ballss3  46029  iinssiin  46065  eliind2  46066  rabssd  46078  choicefi  46135  iunmapss  46149  iunmapsn  46151  axccdom  46156  mptfnd  46175  ssfiunibd  46246  xralrple2  46288  infxr  46300  xrralrecnnle  46316  xrralrecnnge  46323  supxrunb3  46332  fimaxre4  46333  supxrleubrnmpt  46338  rexabslelem  46350  suprleubrnmpt  46354  uzublem  46362  infxrgelbrnmpt  46386  iooiinicc  46476  iooiinioc  46490  mccl  46532  climsuse  46542  mullimc  46550  mullimcf  46557  limcrecl  46563  limsupre  46573  limcleqr  46576  addlimc  46580  0ellimcdiv  46581  limclner  46583  limsupubuzlem  46644  climinf3  46648  limsupequzmpt2  46650  limsupmnfuzlem  46658  limsupre3uzlem  46667  liminfequzmpt2  46723  cncficcgt0  46820  cncfioobd  46829  fprodsubrecnncnvlem  46839  fprodaddrecnncnvlem  46841  dvmptfprodlem  46876  dvnprodlem1  46878  iblsplitf  46902  stoweidlem5  46937  stoweidlem16  46948  stoweidlem18  46950  stoweidlem21  46953  stoweidlem26  46958  stoweidlem27  46959  stoweidlem28  46960  stoweidlem29  46961  stoweidlem31  46963  stoweidlem34  46966  stoweidlem36  46968  stoweidlem41  46973  stoweidlem42  46974  stoweidlem44  46976  stoweidlem45  46977  stoweidlem48  46980  stoweidlem51  46983  stoweidlem55  46987  stoweidlem59  46991  stoweidlem60  46992  stoweidlem62  46994  wallispilem3  46999  stirlinglem5  47010  fourierdlem16  47055  fourierdlem21  47060  fourierdlem22  47061  fourierdlem31  47070  fourierdlem39  47078  fourierdlem68  47106  fourierdlem71  47109  fourierdlem73  47111  fourierdlem77  47115  fourierdlem80  47118  fourierdlem83  47121  fourierdlem87  47125  fourierdlem94  47132  fourierdlem103  47141  fourierdlem104  47142  fourierdlem112  47150  etransclem32  47198  subsaliuncllem  47289  sge0revalmpt  47310  sge0fodjrnlem  47348  sge0fsummptf  47368  iundjiun  47392  meadjiun  47398  voliunsge0lem  47404  meaiininclem  47418  omeiunle  47449  hoicvrrex  47488  ovnsubaddlem2  47503  hoissrrn2  47510  hoidmv1lelem1  47523  hoidmvlelem3  47529  ovnhoilem1  47533  hoi2toco  47539  ovnlecvr2  47542  hspdifhsp  47548  hoiqssbllem1  47554  hoiqssbllem3  47556  hspmbllem2  47559  iinhoiicclem  47605  iunhoiioolem  47607  vonioo  47614  vonicc  47617  pimconstlt0  47633  pimconstlt1  47634  pimltpnff  47635  pimiooltgt  47642  pimdecfgtioc  47647  pimincfltioc  47648  pimdecfgtioo  47649  pimincfltioo  47650  pimgtmnff  47654  issmfd  47667  issmfdf  47669  issmfle  47677  issmfdmpt  47680  issmfgt  47688  issmfled  47689  issmfgtd  47693  smflimlem2  47704  smfmullem4  47726  smfpimcclem  47739  smfsuplem1  47743  smfinflem  47749  iccelpart  48437  mogoldbb  48805  sbgoldbo  48807  pgindnf  50731  aacllem  50861