Theorem ralrimi 3233

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-ral 3045

This theorem is referenced by:  ralrimia  3234  ralimdaa  3236  reximdai  3237  r19.37  3238  rexlimd2  3241  r19.12  3285  ralcom2  3348  rabbidaOLD  3441  2rmorex  3722  iineq2d  4975  disjxiun  5099  rnmpt0f  6204  fnmptd  6641  mpteqb  6969  fmptdf  7071  eusvobj2  7361  offval2f  7648  zfrep6  7913  frrlem4  8245  tfr3  8344  tz7.49  8390  mapxpen  9084  dfac2b  10060  hsmexlem4  10358  axcc3  10367  domtriomlem  10371  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  ac6num  10408  dedekind  11313  dedekindle  11314  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  fprodcllemf  15900  lcmfunsnlem1  16583  lcmfunsnlem2lem1  16584  lcmfunsnlem2  16586  mreexexd  17589  cpmatmcllem  22638  ptcnplem  23541  xkocnv  23734  cfilucfil  24480  cncfcompt2  24834  itg2splitlem  25682  itg2split  25683  itgeq1fOLD  25706  mptelee  28875  lfgrnloop  29105  foresf1o  32483  iinabrex  32548  funimass4f  32611  fcomptf  32632  aciunf1lem  32636  funcnvmpt  32641  fnpreimac  32645  prodindf  32836  isarchiofld  33168  reff  33822  locfinreflem  33823  zarclsiin  33854  zarcmplem  33864  esumeq12dvaf  34014  esumgsum  34028  esumel  34030  esumf1o  34033  esumc  34034  esummono  34037  gsumesum  34042  esumlub  34043  esumlef  34045  esumfsup  34053  esumpinfval  34056  esumpinfsum  34060  esum2d  34076  ldsysgenld  34143  sigapildsyslem  34144  ldgenpisyslem1  34146  measinblem  34203  voliune  34212  volmeas  34214  oms0  34281  omssubadd  34284  dstrvprob  34456  bnj1379  34813  bnj1204  34995  bnj1388  35016  bnj1417  35024  bnj1489  35039  untsucf  35690  domalom  37385  fvineqsneq  37393  cover2  37702  upixp  37716  indexdom  37721  filbcmb  37727  sdclem2  37729  eq0rabdioph  42757  eqrabdioph  42758  setindtr  43006  gneispace  44116  mnuprdlem3  44256  iunconnlem2  44917  rzalf  45004  fnchoice  45016  refsumcn  45017  rfcnnnub  45023  refsum2cnlem1  45024  iuneq2df  45034  uzwo4  45040  ixpeq2d  45055  ixpssmapc  45060  elintd  45061  ssdf  45062  ralimralim  45068  nelrnmpt  45071  ixpssixp  45079  ballss3  45080  iinssiin  45116  eliind2  45117  rabssd  45129  ss2rabdf  45137  choicefi  45187  iunmapss  45202  iunmapsn  45204  axccdom  45209  mptfnd  45229  ssfiunibd  45300  xralrple2  45343  infxr  45356  xrralrecnnle  45372  xrralrecnnge  45379  supxrunb3  45388  fimaxre4  45390  supxrleubrnmpt  45395  rexabslelem  45407  suprleubrnmpt  45411  uzublem  45419  infxrgelbrnmpt  45443  iooiinicc  45533  iooiinioc  45547  mccl  45589  climsuse  45599  mullimc  45607  mullimcf  45614  limcrecl  45620  limsupre  45632  limcleqr  45635  addlimc  45639  0ellimcdiv  45640  limclner  45642  limsupubuzlem  45703  climinf3  45707  limsupequzmpt2  45709  limsupmnfuzlem  45717  limsupre3uzlem  45726  liminfequzmpt2  45782  cncficcgt0  45879  cncfioobd  45888  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  dvmptfprodlem  45935  dvnprodlem1  45937  iblsplitf  45961  stoweidlem5  45996  stoweidlem16  46007  stoweidlem18  46009  stoweidlem21  46012  stoweidlem26  46017  stoweidlem27  46018  stoweidlem28  46019  stoweidlem29  46020  stoweidlem31  46022  stoweidlem34  46025  stoweidlem36  46027  stoweidlem41  46032  stoweidlem42  46033  stoweidlem44  46035  stoweidlem45  46036  stoweidlem48  46039  stoweidlem51  46042  stoweidlem55  46046  stoweidlem59  46050  stoweidlem60  46051  stoweidlem62  46053  wallispilem3  46058  stirlinglem5  46069  fourierdlem16  46114  fourierdlem21  46119  fourierdlem22  46120  fourierdlem31  46129  fourierdlem39  46137  fourierdlem68  46165  fourierdlem71  46168  fourierdlem73  46170  fourierdlem77  46174  fourierdlem80  46177  fourierdlem83  46180  fourierdlem87  46184  fourierdlem94  46191  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  fourierdlem113  46210  etransclem32  46257  subsaliuncllem  46348  sge0revalmpt  46369  sge0fodjrnlem  46407  sge0fsummptf  46427  iundjiun  46451  meadjiun  46457  voliunsge0lem  46463  meaiininclem  46477  omeiunle  46508  hoicvrrex  46547  ovnsubaddlem2  46562  hoissrrn2  46569  hoidmv1lelem1  46582  hoidmvlelem3  46588  ovnhoilem1  46592  hoi2toco  46598  ovnlecvr2  46601  hspdifhsp  46607  hoiqssbllem1  46613  hoiqssbllem3  46615  hspmbllem2  46618  iinhoiicclem  46664  iunhoiioolem  46666  vonioo  46673  vonicc  46676  pimconstlt0  46692  pimconstlt1  46693  pimltpnff  46694  pimiooltgt  46701  pimdecfgtioc  46706  pimincfltioc  46707  pimdecfgtioo  46708  pimincfltioo  46709  preimageiingt  46711  preimaleiinlt  46712  pimgtmnff  46713  issmfd  46726  issmfdf  46728  sssmf  46729  issmfle  46736  issmfdmpt  46739  issmfgt  46747  issmfled  46748  issmfgtd  46752  smflimlem2  46763  smfmullem4  46785  smfpimcclem  46798  smfsuplem1  46802  smfinflem  46808  iccelpart  47427  mogoldbb  47779  sbgoldbo  47781  pgindnf  49698  aacllem  49783