Theorem ralrimi 3263

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

Syntax hints:   → wi 4  Ⅎwnf 1781   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782  df-ral 3068

This theorem is referenced by:  ralrimia  3264  ralimdaa  3266  reximdai  3267  r19.37  3268  rexlimd2  3271  r19.12  3320  r19.12OLD  3321  ralcom2  3385  rabbidaOLD  3485  2rmorex  3776  iineq2d  5038  disjxiun  5163  mpteq2daOLD  5265  rnmpt0f  6274  fnmptd  6721  mpteqb  7048  fmptdf  7151  eusvobj2  7440  offval2f  7729  zfrep6  7995  frrlem4  8330  wfrlem4OLD  8368  tfr3  8455  tz7.49  8501  mapxpen  9209  dfac2b  10200  hsmexlem4  10498  axcc3  10507  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  ac6num  10548  dedekind  11453  dedekindle  11454  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  fprodcllemf  16006  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem2  16687  mreexexd  17706  cpmatmcllem  22745  ptcnplem  23650  xkocnv  23843  cfilucfil  24593  cncfcompt2  24953  itg2splitlem  25803  itg2split  25804  itgeq1fOLD  25827  mptelee  28928  lfgrnloop  29160  foresf1o  32532  iinabrex  32591  funimass4f  32656  fcomptf  32676  aciunf1lem  32680  funcnvmpt  32685  fnpreimac  32689  isarchiofld  33312  reff  33785  locfinreflem  33786  zarclsiin  33817  zarcmplem  33827  prodindf  33987  esumeq12dvaf  33995  esumgsum  34009  esumel  34011  esumf1o  34014  esumc  34015  esummono  34018  gsumesum  34023  esumlub  34024  esumlef  34026  esumfsup  34034  esumpinfval  34037  esumpinfsum  34041  esum2d  34057  ldsysgenld  34124  sigapildsyslem  34125  ldgenpisyslem1  34127  measinblem  34184  voliune  34193  volmeas  34195  oms0  34262  omssubadd  34265  dstrvprob  34436  bnj1379  34806  bnj1204  34988  bnj1388  35009  bnj1417  35017  bnj1489  35032  untsucf  35672  domalom  37370  fvineqsneq  37378  cover2  37675  upixp  37689  indexdom  37694  filbcmb  37700  sdclem2  37702  eq0rabdioph  42732  eqrabdioph  42733  setindtr  42981  gneispace  44096  mnuprdlem3  44243  iunconnlem2  44906  rzalf  44917  fnchoice  44929  refsumcn  44930  rfcnnnub  44936  refsum2cnlem1  44937  iuneq2df  44948  uzwo4  44955  ixpeq2d  44970  ixpssmapc  44975  elintd  44976  ssdf  44977  ralimralim  44983  nelrnmpt  44986  ixpssixp  44994  ballss3  44995  iinssiin  45031  eliind2  45032  rabssd  45044  ss2rabdf  45055  choicefi  45107  iunmapss  45122  iunmapsn  45124  axccdom  45129  mptfnd  45150  ssfiunibd  45224  xralrple2  45269  infxr  45282  xrralrecnnle  45298  xrralrecnnge  45305  supxrunb3  45314  fimaxre4  45316  supxrleubrnmpt  45321  rexabslelem  45333  suprleubrnmpt  45337  uzublem  45345  infxrgelbrnmpt  45369  iooiinicc  45460  iooiinioc  45474  mccl  45519  climsuse  45529  mullimc  45537  mullimcf  45544  limcrecl  45550  limsupre  45562  limcleqr  45565  addlimc  45569  0ellimcdiv  45570  limclner  45572  limsupubuzlem  45633  climinf3  45637  limsupequzmpt2  45639  limsupmnfuzlem  45647  limsupre3uzlem  45656  liminfequzmpt2  45712  cncficcgt0  45809  cncfioobd  45818  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  dvmptfprodlem  45865  dvnprodlem1  45867  iblsplitf  45891  stoweidlem5  45926  stoweidlem16  45937  stoweidlem18  45939  stoweidlem21  45942  stoweidlem26  45947  stoweidlem27  45948  stoweidlem28  45949  stoweidlem29  45950  stoweidlem31  45952  stoweidlem34  45955  stoweidlem36  45957  stoweidlem41  45962  stoweidlem42  45963  stoweidlem44  45965  stoweidlem45  45966  stoweidlem48  45969  stoweidlem51  45972  stoweidlem55  45976  stoweidlem59  45980  stoweidlem60  45981  stoweidlem62  45983  wallispilem3  45988  stirlinglem5  45999  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem31  46059  fourierdlem39  46067  fourierdlem68  46095  fourierdlem71  46098  fourierdlem73  46100  fourierdlem77  46104  fourierdlem80  46107  fourierdlem83  46110  fourierdlem87  46114  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem113  46140  etransclem32  46187  subsaliuncllem  46278  sge0revalmpt  46299  sge0fodjrnlem  46337  sge0fsummptf  46357  iundjiun  46381  meadjiun  46387  voliunsge0lem  46393  meaiininclem  46407  omeiunle  46438  hoicvrrex  46477  ovnsubaddlem2  46492  hoissrrn2  46499  hoidmv1lelem1  46512  hoidmvlelem3  46518  ovnhoilem1  46522  hoi2toco  46528  ovnlecvr2  46531  hspdifhsp  46537  hoiqssbllem1  46543  hoiqssbllem3  46545  hspmbllem2  46548  iinhoiicclem  46594  iunhoiioolem  46596  vonioo  46603  vonicc  46606  pimconstlt0  46622  pimconstlt1  46623  pimltpnff  46624  pimiooltgt  46631  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  preimageiingt  46641  preimaleiinlt  46642  pimgtmnff  46643  issmfd  46656  issmfdf  46658  sssmf  46659  issmfle  46666  issmfdmpt  46669  issmfgt  46677  issmfled  46678  issmfgtd  46682  smflimlem2  46693  smfmullem4  46715  smfpimcclem  46728  smfsuplem1  46732  smfinflem  46738  smfinfmpt  46740  iccelpart  47307  mogoldbb  47659  sbgoldbo  47661  pgindnf  48808  aacllem  48895