Theorem ralrimi 3236

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786  df-ral 3053

This theorem is referenced by:  ralrimia  3237  reximdai  3240  r19.37  3241  rexlimd2  3244  r19.12  3287  ralcom2  3340  2rmorex  3701  disjxiun  5083  nelrnmpt  5918  rnmpt0f  6203  fnmptd  6635  mpteqb  6963  fmptdf  7065  eusvobj2  7354  offval2f  7641  zfrep6OLD  7903  frrlem4  8234  tfr3  8333  tz7.49  8379  mapxpen  9076  dfac2b  10048  hsmexlem4  10346  axcc3  10355  domtriomlem  10359  axdc3lem2  10368  axdc3lem4  10370  axdc4lem  10372  ac6num  10396  dedekind  11304  dedekindle  11305  fsuppmapnn0fiublem  13947  fsuppmapnn0fiub  13948  fprodcllemf  15918  lcmfunsnlem1  16601  lcmfunsnlem2lem1  16602  lcmfunsnlem2  16604  mreexexd  17609  cpmatmcllem  22697  ptcnplem  23600  xkocnv  23793  cfilucfil  24538  cncfcompt2  24889  itg2splitlem  25729  itg2split  25730  itgeq1fOLD  25753  bdaypw2n0bndlem  28473  mpteleeOLD  28982  lfgrnloop  29212  foresf1o  32593  iinabrex  32658  funimass4f  32729  fcomptf  32750  aciunf1lem  32754  fnpreimac  32762  prodindf  32941  isarchiofld  33279  reff  34003  locfinreflem  34004  zarclsiin  34035  zarcmplem  34045  esumeq12dvaf  34195  esumgsum  34209  esumel  34211  esumf1o  34214  esumc  34215  esummono  34218  gsumesum  34223  esumlub  34224  esumlef  34226  esumfsup  34234  esumpinfval  34237  esumpinfsum  34241  esum2d  34257  ldsysgenld  34324  sigapildsyslem  34325  ldgenpisyslem1  34327  measinblem  34384  voliune  34393  volmeas  34395  oms0  34461  omssubadd  34464  dstrvprob  34636  bnj1379  34992  bnj1204  35174  bnj1388  35195  bnj1417  35203  bnj1489  35218  untsucf  35912  domalom  37740  fvineqsneq  37748  cover2  38056  upixp  38070  indexdom  38075  filbcmb  38081  sdclem2  38083  eq0rabdioph  43228  eqrabdioph  43229  setindtr  43476  gneispace  44585  mnuprdlem3  44725  iunconnlem2  45385  rzalf  45472  fnchoice  45484  refsumcn  45485  rfcnnnub  45491  refsum2cnlem1  45492  iuneq2df  45502  uzwo4  45508  ixpeq2d  45523  ixpssmapc  45528  elintd  45529  ssdf  45530  ralimralim  45536  ixpssixp  45546  ballss3  45547  iinssiin  45583  eliind2  45584  rabssd  45596  choicefi  45653  iunmapss  45668  iunmapsn  45670  axccdom  45675  mptfnd  45695  ssfiunibd  45766  xralrple2  45808  infxr  45820  xrralrecnnle  45836  xrralrecnnge  45843  supxrunb3  45852  fimaxre4  45853  supxrleubrnmpt  45858  rexabslelem  45870  suprleubrnmpt  45874  uzublem  45882  infxrgelbrnmpt  45906  iooiinicc  45996  iooiinioc  46010  mccl  46052  climsuse  46062  mullimc  46070  mullimcf  46077  limcrecl  46083  limsupre  46093  limcleqr  46096  addlimc  46100  0ellimcdiv  46101  limclner  46103  limsupubuzlem  46164  climinf3  46168  limsupequzmpt2  46170  limsupmnfuzlem  46178  limsupre3uzlem  46187  liminfequzmpt2  46243  cncficcgt0  46340  cncfioobd  46349  fprodsubrecnncnvlem  46359  fprodaddrecnncnvlem  46361  dvmptfprodlem  46396  dvnprodlem1  46398  iblsplitf  46422  stoweidlem5  46457  stoweidlem16  46468  stoweidlem18  46470  stoweidlem21  46473  stoweidlem26  46478  stoweidlem27  46479  stoweidlem28  46480  stoweidlem29  46481  stoweidlem31  46483  stoweidlem34  46486  stoweidlem36  46488  stoweidlem41  46493  stoweidlem42  46494  stoweidlem44  46496  stoweidlem45  46497  stoweidlem48  46500  stoweidlem51  46503  stoweidlem55  46507  stoweidlem59  46511  stoweidlem60  46512  stoweidlem62  46514  wallispilem3  46519  stirlinglem5  46530  fourierdlem16  46575  fourierdlem21  46580  fourierdlem22  46581  fourierdlem31  46590  fourierdlem39  46598  fourierdlem68  46626  fourierdlem71  46629  fourierdlem73  46631  fourierdlem77  46635  fourierdlem80  46638  fourierdlem83  46641  fourierdlem87  46645  fourierdlem94  46652  fourierdlem103  46661  fourierdlem104  46662  fourierdlem112  46670  fourierdlem113  46671  etransclem32  46718  subsaliuncllem  46809  sge0revalmpt  46830  sge0fodjrnlem  46868  sge0fsummptf  46888  iundjiun  46912  meadjiun  46918  voliunsge0lem  46924  meaiininclem  46938  omeiunle  46969  hoicvrrex  47008  ovnsubaddlem2  47023  hoissrrn2  47030  hoidmv1lelem1  47043  hoidmvlelem3  47049  ovnhoilem1  47053  hoi2toco  47059  ovnlecvr2  47062  hspdifhsp  47068  hoiqssbllem1  47074  hoiqssbllem3  47076  hspmbllem2  47079  iinhoiicclem  47125  iunhoiioolem  47127  vonioo  47134  vonicc  47137  pimconstlt0  47153  pimconstlt1  47154  pimltpnff  47155  pimiooltgt  47162  pimdecfgtioc  47167  pimincfltioc  47168  pimdecfgtioo  47169  pimincfltioo  47170  pimgtmnff  47174  issmfd  47187  issmfdf  47189  sssmf  47190  issmfle  47197  issmfdmpt  47200  issmfgt  47208  issmfled  47209  issmfgtd  47213  smflimlem2  47224  smfmullem4  47246  smfpimcclem  47259  smfsuplem1  47263  smfinflem  47269  iccelpart  47911  mogoldbb  48279  sbgoldbo  48281  pgindnf  50209  aacllem  50294