Theorem ralrimi 3252

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2104  ∀wral 3059

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 1911  ax-6 1969  ax-7 2009  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-ex 1780  df-nf 1784  df-ral 3060

This theorem is referenced by:  ralrimia  3253  ralimdaa  3255  reximdai  3256  r19.37  3257  rexlimd2  3260  r19.12  3309  r19.12OLD  3310  ralcom2  3371  rabbidaOLD  3468  2rmorex  3749  iineq2d  5019  disjxiun  5144  mpteq2daOLD  5246  rnmpt0f  6241  fnmptd  6690  mpteqb  7016  fmptdf  7117  eusvobj2  7403  offval2f  7687  zfrep6  7943  frrlem4  8276  wfrlem4OLD  8314  tfr3  8401  tz7.49  8447  mapxpen  9145  dfac2b  10127  hsmexlem4  10426  axcc3  10435  domtriomlem  10439  axdc3lem2  10448  axdc3lem4  10450  axdc4lem  10452  ac6num  10476  dedekind  11381  dedekindle  11382  fsuppmapnn0fiublem  13959  fsuppmapnn0fiub  13960  fprodcllemf  15906  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmfunsnlem2  16581  mreexexd  17596  cpmatmcllem  22440  ptcnplem  23345  xkocnv  23538  cfilucfil  24288  cncfcompt2  24648  itg2splitlem  25498  itg2split  25499  itgeq1f  25521  mptelee  28420  lfgrnloop  28652  foresf1o  32009  iinabrex  32067  funimass4f  32128  fcomptf  32150  aciunf1lem  32154  funcnvmpt  32159  fnpreimac  32163  isarchiofld  32705  reff  33117  locfinreflem  33118  zarclsiin  33149  zarcmplem  33159  prodindf  33319  esumeq12dvaf  33327  esumgsum  33341  esumel  33343  esumf1o  33346  esumc  33347  esummono  33350  gsumesum  33355  esumlub  33356  esumlef  33358  esumfsup  33366  esumpinfval  33369  esumpinfsum  33373  esum2d  33389  ldsysgenld  33456  sigapildsyslem  33457  ldgenpisyslem1  33459  measinblem  33516  voliune  33525  volmeas  33527  oms0  33594  omssubadd  33597  dstrvprob  33768  bnj1379  34139  bnj1204  34321  bnj1388  34342  bnj1417  34350  bnj1489  34365  untsucf  34983  domalom  36588  fvineqsneq  36596  cover2  36886  upixp  36900  indexdom  36905  filbcmb  36911  sdclem2  36913  eq0rabdioph  41816  eqrabdioph  41817  setindtr  42065  gneispace  43187  mnuprdlem3  43335  iunconnlem2  43998  rzalf  44003  fnchoice  44015  refsumcn  44016  rfcnnnub  44022  refsum2cnlem1  44023  iuneq2df  44034  uzwo4  44041  ixpeq2d  44056  ixpssmapc  44062  elintd  44064  ssdf  44065  ralimralim  44071  nelrnmpt  44074  ixpssixp  44082  ballss3  44083  iinssiin  44119  eliind2  44120  rabssd  44132  ss2rabdf  44145  choicefi  44197  iunmapss  44212  iunmapsn  44214  axccdom  44219  mptfnd  44243  ssfiunibd  44317  xralrple2  44362  infxr  44375  xrralrecnnle  44391  xrralrecnnge  44398  supxrunb3  44407  fimaxre4  44409  supxrleubrnmpt  44414  rexabslelem  44426  suprleubrnmpt  44430  uzublem  44438  infxrgelbrnmpt  44462  iooiinicc  44553  iooiinioc  44567  mccl  44612  climsuse  44622  mullimc  44630  mullimcf  44637  limcrecl  44643  limsupre  44655  limcleqr  44658  addlimc  44662  0ellimcdiv  44663  limclner  44665  limsupubuzlem  44726  climinf3  44730  limsupequzmpt2  44732  limsupmnfuzlem  44740  limsupre3uzlem  44749  liminfequzmpt2  44805  cncficcgt0  44902  cncfioobd  44911  fprodsubrecnncnvlem  44921  fprodaddrecnncnvlem  44923  dvmptfprodlem  44958  dvnprodlem1  44960  iblsplitf  44984  stoweidlem5  45019  stoweidlem16  45030  stoweidlem18  45032  stoweidlem21  45035  stoweidlem26  45040  stoweidlem27  45041  stoweidlem28  45042  stoweidlem29  45043  stoweidlem31  45045  stoweidlem34  45048  stoweidlem36  45050  stoweidlem41  45055  stoweidlem42  45056  stoweidlem44  45058  stoweidlem45  45059  stoweidlem48  45062  stoweidlem51  45065  stoweidlem55  45069  stoweidlem59  45073  stoweidlem60  45074  stoweidlem62  45076  wallispilem3  45081  stirlinglem5  45092  fourierdlem16  45137  fourierdlem21  45142  fourierdlem22  45143  fourierdlem31  45152  fourierdlem39  45160  fourierdlem68  45188  fourierdlem71  45191  fourierdlem73  45193  fourierdlem77  45197  fourierdlem80  45200  fourierdlem83  45203  fourierdlem87  45207  fourierdlem94  45214  fourierdlem103  45223  fourierdlem104  45224  fourierdlem112  45232  fourierdlem113  45233  etransclem32  45280  subsaliuncllem  45371  sge0revalmpt  45392  sge0fodjrnlem  45430  sge0fsummptf  45450  iundjiun  45474  meadjiun  45480  voliunsge0lem  45486  meaiininclem  45500  omeiunle  45531  hoicvrrex  45570  ovnsubaddlem2  45585  hoissrrn2  45592  hoidmv1lelem1  45605  hoidmvlelem3  45611  ovnhoilem1  45615  hoi2toco  45621  ovnlecvr2  45624  hspdifhsp  45630  hoiqssbllem1  45636  hoiqssbllem3  45638  hspmbllem2  45641  iinhoiicclem  45687  iunhoiioolem  45689  vonioo  45696  vonicc  45699  pimconstlt0  45715  pimconstlt1  45716  pimltpnff  45717  pimiooltgt  45724  pimdecfgtioc  45729  pimincfltioc  45730  pimdecfgtioo  45731  pimincfltioo  45732  preimageiingt  45734  preimaleiinlt  45735  pimgtmnff  45736  issmfd  45749  issmfdf  45751  sssmf  45752  issmfle  45759  issmfdmpt  45762  issmfgt  45770  issmfled  45771  issmfgtd  45775  smflimlem2  45786  smfmullem4  45808  smfpimcclem  45821  smfsuplem1  45825  smfinflem  45831  smfinfmpt  45833  iccelpart  46399  mogoldbb  46751  sbgoldbo  46753  pgindnf  47848  aacllem  47935