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 1815   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816  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  5948  rnmpt0f  6244  fnmptd  6680  mpteqb  7013  fmptdf  7117  eusvobj2  7412  offval2f  7708  zfrep6OLD  7967  frrlem4  8308  tfr3  8408  tz7.49  8456  mapxpen  9163  dfac2b  10210  hsmexlem4  10508  axcc3  10517  domtriomlem  10521  axdc3lem2  10530  axdc3lem4  10532  axdc4lem  10534  ac6num  10558  dedekind  11474  dedekindle  11475  fsuppmapnn0fiublem  14134  fsuppmapnn0fiub  14135  fprodcllemf  16126  lcmfunsnlem1  16813  lcmfunsnlem2lem1  16814  lcmfunsnlem2  16816  mreexexd  17823  cpmatmcllem  23037  ptcnplem  23941  xkocnv  24134  cfilucfil  24879  cncfcompt2  25230  itg2splitlem  26070  itg2split  26071  bdaypw2n0bndlem  28850  mpteleeOLD  29474  lfgrnloop  29704  foresf1o  33143  iinabrex  33206  funimass4f  33274  fcomptf  33295  aciunf1lem  33299  fnpreimac  33307  prodindf  33472  isarchiofld  33803  reff  34514  locfinreflem  34515  zarclsiin  34546  zarcmplem  34556  esumeq12dvaf  34706  esumgsum  34720  esumel  34722  esumf1o  34725  esumc  34726  esummono  34729  gsumesum  34734  esumlub  34735  esumlef  34737  esumfsup  34745  esumpinfval  34748  esumpinfsum  34752  esum2d  34768  ldsysgenld  34836  sigapildsyslem  34837  ldgenpisyslem1  34839  measinblem  34896  voliune  34905  volmeas  34907  oms0  34972  omssubadd  34975  dstrvprob  35147  bnj1379  35503  bnj1204  35685  bnj1388  35706  bnj1417  35714  bnj1489  35729  untsucf  36550  domalom  38403  fvineqsneq  38411  cover2  38725  upixp  38739  indexdom  38744  filbcmb  38750  sdclem2  38752  eq0rabdioph  43863  eqrabdioph  43864  setindtr  44107  gneispace  45210  mnuprdlem3  45334  iunconnlem2  45993  rzalf  46110  fnchoice  46122  refsumcn  46123  rfcnnnub  46129  refsum2cnlem1  46130  iuneq2df  46140  uzwo4  46146  ixpeq2d  46161  ixpssmapc  46166  elintd  46167  ssdf  46168  ralimralim  46174  ixpssixp  46183  ballss3  46184  iinssiin  46220  eliind2  46221  rabssd  46233  choicefi  46290  iunmapss  46304  iunmapsn  46306  axccdom  46311  mptfnd  46330  ssfiunibd  46401  xralrple2  46442  infxr  46454  xrralrecnnle  46470  xrralrecnnge  46477  supxrunb3  46486  fimaxre4  46487  supxrleubrnmpt  46492  rexabslelem  46504  suprleubrnmpt  46508  uzublem  46516  infxrgelbrnmpt  46540  iooiinicc  46630  iooiinioc  46644  mccl  46686  climsuse  46696  mullimc  46704  mullimcf  46711  limcrecl  46717  limsupre  46727  limcleqr  46730  addlimc  46734  0ellimcdiv  46735  limclner  46737  limsupubuzlem  46798  climinf3  46802  limsupequzmpt2  46804  limsupmnfuzlem  46812  limsupre3uzlem  46821  liminfequzmpt2  46877  cncficcgt0  46974  cncfioobd  46983  fprodsubrecnncnvlem  46993  fprodaddrecnncnvlem  46995  dvmptfprodlem  47030  dvnprodlem1  47032  iblsplitf  47056  stoweidlem5  47091  stoweidlem16  47102  stoweidlem18  47104  stoweidlem21  47107  stoweidlem26  47112  stoweidlem27  47113  stoweidlem28  47114  stoweidlem29  47115  stoweidlem31  47117  stoweidlem34  47120  stoweidlem36  47122  stoweidlem41  47127  stoweidlem42  47128  stoweidlem44  47130  stoweidlem45  47131  stoweidlem48  47134  stoweidlem51  47137  stoweidlem55  47141  stoweidlem59  47145  stoweidlem60  47146  stoweidlem62  47148  wallispilem3  47153  stirlinglem5  47164  fourierdlem16  47209  fourierdlem21  47214  fourierdlem22  47215  fourierdlem31  47224  fourierdlem39  47232  fourierdlem68  47260  fourierdlem71  47263  fourierdlem73  47265  fourierdlem77  47269  fourierdlem80  47272  fourierdlem83  47275  fourierdlem87  47279  fourierdlem94  47286  fourierdlem103  47295  fourierdlem104  47296  fourierdlem112  47304  etransclem32  47352  subsaliuncllem  47443  sge0revalmpt  47464  sge0fodjrnlem  47502  sge0fsummptf  47522  iundjiun  47546  meadjiun  47552  voliunsge0lem  47558  meaiininclem  47572  omeiunle  47603  hoicvrrex  47642  ovnsubaddlem2  47657  hoissrrn2  47664  hoidmv1lelem1  47677  hoidmvlelem3  47683  ovnhoilem1  47687  hoi2toco  47693  ovnlecvr2  47696  hspdifhsp  47702  hoiqssbllem1  47708  hoiqssbllem3  47710  hspmbllem2  47713  iinhoiicclem  47759  iunhoiioolem  47761  vonioo  47768  vonicc  47771  pimconstlt0  47787  pimconstlt1  47788  pimltpnff  47789  pimiooltgt  47796  pimdecfgtioc  47801  pimincfltioc  47802  pimdecfgtioo  47803  pimincfltioo  47804  pimgtmnff  47808  issmfd  47821  issmfdf  47823  issmfle  47831  issmfdmpt  47834  issmfgt  47842  issmfled  47843  issmfgtd  47847  smflimlem2  47858  smfmullem4  47880  smfpimcclem  47893  smfsuplem1  47897  smfinflem  47903  iccelpart  48591  mogoldbb  48959  sbgoldbo  48961  pgindnf  50885  aacllem  51015