Theorem ralrimi 3264

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

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

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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  ralrimia  3265  reximdai  3268  r19.37  3269  rexlimd2  3272  r19.12  3315  ralcom2  3366  2rmorex  3715  disjxiun  5103  nelrnmpt  5956  rnmpt0f  6257  fnmptd  6702  mpteqb  7036  fmptdf  7141  eusvobj2  7435  offval2f  7732  zfrep6OLD  7991  frrlem4  8335  tfr3  8435  tz7.49  8483  mapxpen  9190  dfac2b  10236  hsmexlem4  10534  axcc3  10543  domtriomlem  10547  axdc3lem2  10556  axdc3lem4  10558  axdc4lem  10560  ac6num  10584  dedekind  11500  dedekindle  11501  fsuppmapnn0fiublem  14160  fsuppmapnn0fiub  14161  fprodcllemf  16154  lcmfunsnlem1  16841  lcmfunsnlem2lem1  16842  lcmfunsnlem2  16844  mreexexd  17851  cpmatmcllem  23066  ptcnplem  23970  xkocnv  24163  cfilucfil  24908  cncfcompt2  25259  itg2splitlem  26099  itg2split  26100  bdaypw2n0bndlem  28879  mpteleeOLD  29503  lfgrnloop  29733  iinabrex  33235  funimass4f  33303  fcomptf  33324  aciunf1lem  33328  fnpreimac  33336  prodindf  33499  isarchiofld  33830  locfinreflem  34542  zarclsiin  34573  zarcmplem  34583  esumeq12dvaf  34733  esumgsum  34747  esumel  34749  esumf1o  34752  esumc  34753  esummono  34756  gsumesum  34761  esumlub  34762  esumlef  34764  esumfsup  34772  esumpinfval  34775  esumpinfsum  34779  esum2d  34795  ldsysgenld  34863  sigapildsyslem  34864  ldgenpisyslem1  34866  measinblem  34923  voliune  34932  volmeas  34934  oms0  34999  dstrvprob  35174  bnj1379  35530  bnj1204  35712  bnj1388  35733  bnj1417  35741  bnj1489  35756  untsucf  36653  domalom  38519  fvineqsneq  38527  cover2  38841  upixp  38855  indexdom  38860  filbcmb  38866  sdclem2  38868  eq0rabdioph  43980  eqrabdioph  43981  setindtr  44224  gneispace  45326  mnuprdlem3  45450  iunconnlem2  46108  rzalf  46239  fnchoice  46251  refsumcn  46252  rfcnnnub  46258  refsum2cnlem1  46259  iuneq2df  46269  uzwo4  46275  ixpeq2d  46290  ixpssmapc  46295  elintd  46296  ssdf  46297  ralimralim  46303  ixpssixp  46312  ballss3  46313  iinssiin  46349  eliind2  46350  rabssd  46362  choicefi  46419  iunmapss  46433  iunmapsn  46435  axccdom  46440  mptfnd  46459  ssfiunibd  46530  xralrple2  46571  infxr  46583  xrralrecnnle  46599  xrralrecnnge  46606  supxrunb3  46615  fimaxre4  46616  supxrleubrnmpt  46621  rexabslelem  46633  suprleubrnmpt  46637  uzublem  46645  infxrgelbrnmpt  46669  iooiinicc  46759  iooiinioc  46773  mccl  46815  climsuse  46825  mullimc  46833  mullimcf  46840  limcrecl  46846  limsupre  46856  limcleqr  46859  addlimc  46863  0ellimcdiv  46864  limclner  46866  limsupubuzlem  46927  climinf3  46931  limsupequzmpt2  46933  limsupmnfuzlem  46941  limsupre3uzlem  46950  liminfequzmpt2  47006  cncficcgt0  47103  cncfioobd  47112  fprodsubrecnncnvlem  47122  fprodaddrecnncnvlem  47124  dvmptfprodlem  47159  dvnprodlem1  47161  iblsplitf  47185  stoweidlem5  47220  stoweidlem16  47231  stoweidlem18  47233  stoweidlem21  47236  stoweidlem26  47241  stoweidlem27  47242  stoweidlem28  47243  stoweidlem29  47244  stoweidlem31  47246  stoweidlem34  47249  stoweidlem36  47251  stoweidlem41  47256  stoweidlem42  47257  stoweidlem44  47259  stoweidlem45  47260  stoweidlem48  47263  stoweidlem51  47266  stoweidlem55  47270  stoweidlem59  47274  stoweidlem60  47275  stoweidlem62  47277  wallispilem3  47282  stirlinglem5  47293  fourierdlem16  47338  fourierdlem21  47343  fourierdlem22  47344  fourierdlem31  47353  fourierdlem39  47361  fourierdlem68  47389  fourierdlem71  47392  fourierdlem73  47394  fourierdlem77  47398  fourierdlem80  47401  fourierdlem83  47404  fourierdlem87  47408  fourierdlem94  47415  fourierdlem103  47424  fourierdlem104  47425  fourierdlem112  47433  etransclem32  47481  subsaliuncllem  47572  sge0revalmpt  47593  sge0fodjrnlem  47631  sge0fsummptf  47651  iundjiun  47675  meadjiun  47681  voliunsge0lem  47687  meaiininclem  47701  omeiunle  47732  hoicvrrex  47771  ovnsubaddlem2  47786  hoissrrn2  47793  hoidmv1lelem1  47806  hoidmvlelem3  47812  ovnhoilem1  47816  hoi2toco  47822  ovnlecvr2  47825  hspdifhsp  47831  hoiqssbllem1  47837  hoiqssbllem3  47839  hspmbllem2  47842  iinhoiicclem  47888  iunhoiioolem  47890  vonioo  47897  vonicc  47900  pimconstlt0  47916  pimconstlt1  47917  pimltpnff  47918  pimiooltgt  47925  pimdecfgtioc  47930  pimincfltioc  47931  pimdecfgtioo  47932  pimincfltioo  47933  pimgtmnff  47937  issmfd  47950  issmfdf  47952  issmfle  47960  issmfdmpt  47963  issmfgt  47971  issmfled  47972  issmfgtd  47976  smflimlem2  47987  smfmullem4  48009  smfpimcclem  48022  smfsuplem1  48026  smfinflem  48032  iccelpart  48720  mogoldbb  49088  sbgoldbo  49090  pgindnf  51089  aacllem  51219