Theorem ralrimi 3230

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2111  ∀wral 3047

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 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785  df-ral 3048

This theorem is referenced by:  ralrimia  3231  ralimdaa  3233  reximdai  3234  r19.37  3235  rexlimd2  3238  r19.12  3281  ralcom2  3343  rabbidaOLD  3433  2rmorex  3708  iineq2d  4963  disjxiun  5086  rnmpt0f  6190  fnmptd  6622  mpteqb  6948  fmptdf  7050  eusvobj2  7338  offval2f  7625  zfrep6  7887  frrlem4  8219  tfr3  8318  tz7.49  8364  mapxpen  9056  dfac2b  10022  hsmexlem4  10320  axcc3  10329  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  axdc4lem  10346  ac6num  10370  dedekind  11276  dedekindle  11277  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  fprodcllemf  15865  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  mreexexd  17554  cpmatmcllem  22633  ptcnplem  23536  xkocnv  23729  cfilucfil  24474  cncfcompt2  24828  itg2splitlem  25676  itg2split  25677  itgeq1fOLD  25700  mptelee  28873  lfgrnloop  29103  foresf1o  32484  iinabrex  32549  funimass4f  32619  fcomptf  32640  aciunf1lem  32644  funcnvmpt  32649  fnpreimac  32653  prodindf  32844  isarchiofld  33168  reff  33852  locfinreflem  33853  zarclsiin  33884  zarcmplem  33894  esumeq12dvaf  34044  esumgsum  34058  esumel  34060  esumf1o  34063  esumc  34064  esummono  34067  gsumesum  34072  esumlub  34073  esumlef  34075  esumfsup  34083  esumpinfval  34086  esumpinfsum  34090  esum2d  34106  ldsysgenld  34173  sigapildsyslem  34174  ldgenpisyslem1  34176  measinblem  34233  voliune  34242  volmeas  34244  oms0  34310  omssubadd  34313  dstrvprob  34485  bnj1379  34842  bnj1204  35024  bnj1388  35045  bnj1417  35053  bnj1489  35068  untsucf  35754  domalom  37448  fvineqsneq  37456  cover2  37754  upixp  37768  indexdom  37773  filbcmb  37779  sdclem2  37781  eq0rabdioph  42868  eqrabdioph  42869  setindtr  43116  gneispace  44226  mnuprdlem3  44366  iunconnlem2  45026  rzalf  45113  fnchoice  45125  refsumcn  45126  rfcnnnub  45132  refsum2cnlem1  45133  iuneq2df  45143  uzwo4  45149  ixpeq2d  45164  ixpssmapc  45169  elintd  45170  ssdf  45171  ralimralim  45177  nelrnmpt  45180  ixpssixp  45188  ballss3  45189  iinssiin  45225  eliind2  45226  rabssd  45238  ss2rabdf  45246  choicefi  45296  iunmapss  45311  iunmapsn  45313  axccdom  45318  mptfnd  45338  ssfiunibd  45409  xralrple2  45452  infxr  45464  xrralrecnnle  45480  xrralrecnnge  45487  supxrunb3  45496  fimaxre4  45498  supxrleubrnmpt  45503  rexabslelem  45515  suprleubrnmpt  45519  uzublem  45527  infxrgelbrnmpt  45551  iooiinicc  45641  iooiinioc  45655  mccl  45697  climsuse  45707  mullimc  45715  mullimcf  45722  limcrecl  45728  limsupre  45738  limcleqr  45741  addlimc  45745  0ellimcdiv  45746  limclner  45748  limsupubuzlem  45809  climinf3  45813  limsupequzmpt2  45815  limsupmnfuzlem  45823  limsupre3uzlem  45832  liminfequzmpt2  45888  cncficcgt0  45985  cncfioobd  45994  fprodsubrecnncnvlem  46004  fprodaddrecnncnvlem  46006  dvmptfprodlem  46041  dvnprodlem1  46043  iblsplitf  46067  stoweidlem5  46102  stoweidlem16  46113  stoweidlem18  46115  stoweidlem21  46118  stoweidlem26  46123  stoweidlem27  46124  stoweidlem28  46125  stoweidlem29  46126  stoweidlem31  46128  stoweidlem34  46131  stoweidlem36  46133  stoweidlem41  46138  stoweidlem42  46139  stoweidlem44  46141  stoweidlem45  46142  stoweidlem48  46145  stoweidlem51  46148  stoweidlem55  46152  stoweidlem59  46156  stoweidlem60  46157  stoweidlem62  46159  wallispilem3  46164  stirlinglem5  46175  fourierdlem16  46220  fourierdlem21  46225  fourierdlem22  46226  fourierdlem31  46235  fourierdlem39  46243  fourierdlem68  46271  fourierdlem71  46274  fourierdlem73  46276  fourierdlem77  46280  fourierdlem80  46283  fourierdlem83  46286  fourierdlem87  46290  fourierdlem94  46297  fourierdlem103  46306  fourierdlem104  46307  fourierdlem112  46315  fourierdlem113  46316  etransclem32  46363  subsaliuncllem  46454  sge0revalmpt  46475  sge0fodjrnlem  46513  sge0fsummptf  46533  iundjiun  46557  meadjiun  46563  voliunsge0lem  46569  meaiininclem  46583  omeiunle  46614  hoicvrrex  46653  ovnsubaddlem2  46668  hoissrrn2  46675  hoidmv1lelem1  46688  hoidmvlelem3  46694  ovnhoilem1  46698  hoi2toco  46704  ovnlecvr2  46707  hspdifhsp  46713  hoiqssbllem1  46719  hoiqssbllem3  46721  hspmbllem2  46724  iinhoiicclem  46770  iunhoiioolem  46772  vonioo  46779  vonicc  46782  pimconstlt0  46798  pimconstlt1  46799  pimltpnff  46800  pimiooltgt  46807  pimdecfgtioc  46812  pimincfltioc  46813  pimdecfgtioo  46814  pimincfltioo  46815  preimageiingt  46817  preimaleiinlt  46818  pimgtmnff  46819  issmfd  46832  issmfdf  46834  sssmf  46835  issmfle  46842  issmfdmpt  46845  issmfgt  46853  issmfled  46854  issmfgtd  46858  smflimlem2  46869  smfmullem4  46891  smfpimcclem  46904  smfsuplem1  46908  smfinflem  46914  iccelpart  47532  mogoldbb  47884  sbgoldbo  47886  pgindnf  49816  aacllem  49901