Theorem ralrimi 3262

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

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

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 2215

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

This theorem is used by:  ralrimia  3263  reximdai  3266  r19.37  3267  rexlimd2  3270  r19.12  3313  ralcom2  3364  2rmorex  3715  disjxiun  5104  nelrnmpt  5955  rnmpt0f  6243  fnmptd  6677  mpteqb  7010  fmptdf  7113  eusvobj2  7408  offval2f  7696  zfrep6OLD  7955  frrlem4  8291  tfr3  8391  tz7.49  8437  mapxpen  9144  dfac2b  10136  hsmexlem4  10434  axcc3  10443  domtriomlem  10447  axdc3lem2  10456  axdc3lem4  10458  axdc4lem  10460  ac6num  10484  dedekind  11400  dedekindle  11401  fsuppmapnn0fiublem  14056  fsuppmapnn0fiub  14057  fprodcllemf  16049  lcmfunsnlem1  16731  lcmfunsnlem2lem1  16732  lcmfunsnlem2  16734  mreexexd  17740  cpmatmcllem  22944  ptcnplem  23848  xkocnv  24041  cfilucfil  24786  cncfcompt2  25137  itg2splitlem  25977  itg2split  25978  itgeq1fOLD  26001  bdaypw2n0bndlem  28726  mpteleeOLD  29338  lfgrnloop  29568  foresf1o  32965  iinabrex  33029  funimass4f  33097  fcomptf  33118  aciunf1lem  33122  fnpreimac  33130  prodindf  33295  isarchiofld  33626  reff  34336  locfinreflem  34337  zarclsiin  34368  zarcmplem  34378  esumeq12dvaf  34528  esumgsum  34542  esumel  34544  esumf1o  34547  esumc  34548  esummono  34551  gsumesum  34556  esumlub  34557  esumlef  34559  esumfsup  34567  esumpinfval  34570  esumpinfsum  34574  esum2d  34590  ldsysgenld  34658  sigapildsyslem  34659  ldgenpisyslem1  34661  measinblem  34718  voliune  34727  volmeas  34729  oms0  34795  omssubadd  34798  dstrvprob  34970  bnj1379  35326  bnj1204  35508  bnj1388  35529  bnj1417  35537  bnj1489  35552  untsucf  36276  domalom  38145  fvineqsneq  38153  cover2  38452  upixp  38466  indexdom  38471  filbcmb  38477  sdclem2  38479  eq0rabdioph  43608  eqrabdioph  43609  setindtr  43852  gneispace  44961  mnuprdlem3  45085  iunconnlem2  45744  rzalf  45838  fnchoice  45850  refsumcn  45851  rfcnnnub  45857  refsum2cnlem1  45858  iuneq2df  45868  uzwo4  45874  ixpeq2d  45889  ixpssmapc  45894  elintd  45895  ssdf  45896  ralimralim  45902  ixpssixp  45911  ballss3  45912  iinssiin  45948  eliind2  45949  rabssd  45961  choicefi  46018  iunmapss  46032  iunmapsn  46034  axccdom  46039  mptfnd  46058  ssfiunibd  46129  xralrple2  46171  infxr  46183  xrralrecnnle  46199  xrralrecnnge  46206  supxrunb3  46215  fimaxre4  46216  supxrleubrnmpt  46221  rexabslelem  46233  suprleubrnmpt  46237  uzublem  46245  infxrgelbrnmpt  46269  iooiinicc  46359  iooiinioc  46373  mccl  46415  climsuse  46425  mullimc  46433  mullimcf  46440  limcrecl  46446  limsupre  46456  limcleqr  46459  addlimc  46463  0ellimcdiv  46464  limclner  46466  limsupubuzlem  46527  climinf3  46531  limsupequzmpt2  46533  limsupmnfuzlem  46541  limsupre3uzlem  46550  liminfequzmpt2  46606  cncficcgt0  46703  cncfioobd  46712  fprodsubrecnncnvlem  46722  fprodaddrecnncnvlem  46724  dvmptfprodlem  46759  dvnprodlem1  46761  iblsplitf  46785  stoweidlem5  46820  stoweidlem16  46831  stoweidlem18  46833  stoweidlem21  46836  stoweidlem26  46841  stoweidlem27  46842  stoweidlem28  46843  stoweidlem29  46844  stoweidlem31  46846  stoweidlem34  46849  stoweidlem36  46851  stoweidlem41  46856  stoweidlem42  46857  stoweidlem44  46859  stoweidlem45  46860  stoweidlem48  46863  stoweidlem51  46866  stoweidlem55  46870  stoweidlem59  46874  stoweidlem60  46875  stoweidlem62  46877  wallispilem3  46882  stirlinglem5  46893  fourierdlem16  46938  fourierdlem21  46943  fourierdlem22  46944  fourierdlem31  46953  fourierdlem39  46961  fourierdlem68  46989  fourierdlem71  46992  fourierdlem73  46994  fourierdlem77  46998  fourierdlem80  47001  fourierdlem83  47004  fourierdlem87  47008  fourierdlem94  47015  fourierdlem103  47024  fourierdlem104  47025  fourierdlem112  47033  etransclem32  47081  subsaliuncllem  47172  sge0revalmpt  47193  sge0fodjrnlem  47231  sge0fsummptf  47251  iundjiun  47275  meadjiun  47281  voliunsge0lem  47287  meaiininclem  47301  omeiunle  47332  hoicvrrex  47371  ovnsubaddlem2  47386  hoissrrn2  47393  hoidmv1lelem1  47406  hoidmvlelem3  47412  ovnhoilem1  47416  hoi2toco  47422  ovnlecvr2  47425  hspdifhsp  47431  hoiqssbllem1  47437  hoiqssbllem3  47439  hspmbllem2  47442  iinhoiicclem  47488  iunhoiioolem  47490  vonioo  47497  vonicc  47500  pimconstlt0  47516  pimconstlt1  47517  pimltpnff  47518  pimiooltgt  47525  pimdecfgtioc  47530  pimincfltioc  47531  pimdecfgtioo  47532  pimincfltioo  47533  pimgtmnff  47537  issmfd  47550  issmfdf  47552  issmfle  47560  issmfdmpt  47563  issmfgt  47571  issmfled  47572  issmfgtd  47576  smflimlem2  47587  smfmullem4  47609  smfpimcclem  47622  smfsuplem1  47626  smfinflem  47632  iccelpart  48320  mogoldbb  48688  sbgoldbo  48690  pgindnf  50629  aacllem  50759