Theorem ralrimiv 3120

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 4-Dec-2019.)

Hypothesis

Ref	Expression
ralrimiv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))

Assertion

Ref	Expression
ralrimiv	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiv

Step	Hyp	Ref	Expression
1		ax-5 1910	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ralrimiv.1	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	hbralrimi 3119	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

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 1910

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  ralrimiva  3121  ralrimivw  3125  ralrimdv  3127  ralrimivv  3170  rr19.3v  3619  class2seteq  3660  rabssdv  4022  rzalALT  4457  disjord  5077  disjiund  5079  trin  5206  ralxfrALT  5350  otiunsndisj  5457  onmindif  6395  fnprb  7136  fntpb  7137  f1cdmsn  7210  ssorduni  7706  onminex  7729  onmindif2  7734  limuni3  7776  frxp  8050  poxp  8052  sexp2  8070  sexp3  8077  onfununi  8255  onnseq  8258  tfrlem12  8302  tz7.48-2  8355  oaass  8470  omass  8489  oelim2  8504  oelimcl  8509  oaabs2  8558  omabs  8560  uniqs  8692  undifixp  8852  dom2lem  8908  isinf  9143  unblem4  9173  unbnn2  9175  marypha1lem  9311  supssd  9341  supiso  9354  infssd  9372  ordiso2  9395  card2inf  9435  elirrvOLD  9478  wemapwe  9581  ttrclss  9604  trcl  9612  frr3g  9640  tz9.13  9675  rankval3b  9710  rankunb  9734  rankuni2b  9737  scott0  9770  updjud  9818  dfac8alem  9911  carduniima  9978  alephsmo  9984  alephval3  9992  iunfictbso  9996  dfac3  10003  dfac5lem5  10009  dfac12r  10029  dfac12k  10030  kmlem4  10036  kmlem11  10043  cfsuc  10139  cofsmo  10151  cfsmolem  10152  coftr  10155  alephsing  10158  infpssrlem3  10187  fin23lem30  10224  isf32lem2  10236  isf32lem3  10237  isf34lem6  10262  fin1a2lem11  10292  fin1a2lem13  10294  fin1a2s  10296  axcc2lem  10318  domtriomlem  10324  axdc3lem2  10333  axdc4lem  10337  axcclem  10339  axdclem2  10402  iundom2g  10422  uniimadom  10426  cardmin  10446  alephval2  10454  alephreg  10464  fpwwe2lem11  10523  wunex2  10620  wuncval2  10629  tskwe2  10655  inar1  10657  tskuni  10665  gruun  10688  intgru  10696  grutsk1  10703  genpcl  10890  ltexprlem5  10922  suplem1pr  10934  supexpr  10936  supsrlem  10993  axpre-sup  11051  negfi  12062  supaddc  12080  supadd  12081  supmul1  12082  supmullem1  12083  supmul  12085  peano5nni  12119  uzind  12556  zindd  12565  uzwo  12800  lbzbi  12825  xrsupsslem  13197  xrinfmsslem  13198  supxrun  13206  supxrpnf  13208  supxrunb1  13209  supxrunb2  13210  icoshftf1o  13365  flval3  13707  axdc4uzlem  13878  tpfo  14395  wrdnfi  14443  ccatrn  14484  ccatalpha  14488  2cshw  14707  cshweqrep  14715  s3iunsndisj  14862  rtrclreclem4  14955  dfrtrcl2  14956  01sqrexlem1  15136  01sqrexlem6  15141  fsum0diag2  15677  alzdvds  16218  gcdcllem1  16397  lcmfunsnlem2lem1  16536  lcmfunsnlem2lem2  16537  maxprmfct  16607  hashgcdeq  16688  unbenlem  16807  vdwlem6  16885  vdwlem10  16889  firest  17323  mrieqv2d  17532  iscatd  17566  initoeu2  17910  setcmon  17981  setcepi  17982  fullestrcsetc  18044  fullsetcestrc  18059  isglbd  18402  isacs4lem  18437  acsfiindd  18446  acsmapd  18447  psss  18473  sgrpidmnd  18600  pwmnd  18798  ghmrn  19095  ghmpreima  19104  cntz2ss  19201  symgextres  19291  psgnunilem2  19361  lsmsubg  19520  efgsfo  19605  gsumzaddlem  19787  gsummptnn0fzfv  19853  dmdprdd  19867  dprd2da  19910  ablsimpgprmd  19983  imasring  20202  01eq0ring  20399  isabvd  20681  issrngd  20724  islssd  20822  lbsextlem3  21051  lbsextlem4  21052  lidldvgen  21225  pzriprnglem4  21375  pzriprnglem7  21378  pzriprnglem13  21384  psgnghm  21471  isphld  21545  frlmsslsp  21687  mp2pm2mplem4  22678  tgcl  22838  distop  22864  indistopon  22870  pptbas  22877  toponmre  22962  opnnei  22989  neiuni  22991  neindisj2  22992  ordtrest2  23073  cnpnei  23133  cnindis  23161  cmpcld  23271  uncmp  23272  hauscmplem  23275  2ndc1stc  23320  1stcrest  23322  1stcelcls  23330  llyrest  23354  nllyrest  23355  cldllycmp  23364  reftr  23383  locfincf  23400  comppfsc  23401  txcls  23473  ptpjcn  23480  ptclsg  23484  dfac14lem  23486  xkoccn  23488  txlly  23505  txnlly  23506  ptrescn  23508  tx1stc  23519  xkoco1cn  23526  xkoco2cn  23527  xkococn  23529  xkoinjcn  23556  qtopeu  23585  hmeofval  23627  ordthmeolem  23670  isfild  23727  fbasrn  23753  trfil2  23756  flimclslem  23853  fclsrest  23893  fclscf  23894  flimfcls  23895  alexsubALTlem1  23916  alexsubALTlem2  23917  alexsubALTlem3  23918  alexsubALT  23920  qustgpopn  23989  isxmetd  24195  imasdsf1olem  24242  blcls  24375  prdsxmslem2  24398  metustfbas  24426  dscmet  24441  nrmmetd  24443  reperflem  24688  reconnlem2  24697  xrge0tsms  24704  fsumcn  24742  cnheibor  24835  tcphcph  25118  lmmbr  25139  caubl  25189  ivthlem1  25333  ovolctb  25372  ovoliunlem2  25385  ovolscalem1  25395  ovolicc2  25404  voliunlem3  25434  ismbfd  25521  mbfimaopnlem  25537  itg2le  25621  ellimc2  25759  c1liplem1  25882  plyeq0lem  26096  dgreq0  26152  aannenlem1  26217  pilem2  26343  cxpcn3lem  26638  scvxcvx  26877  musum  27082  fsumdvdsmul  27086  dchrisum0flb  27402  ostth2lem2  27526  sltval2  27549  nolesgn2ores  27565  nogesgn1ores  27567  nosupres  27600  nosupbnd2lem1  27608  noinfres  27615  noinfbnd2lem1  27623  scutun12  27705  madebdayim  27787  precsexlem9  28107  noseqind  28176  zs12zodd  28346  zs12bday  28348  numedglnl  29076  upgrreslem  29236  umgrreslem  29237  nbuhgr  29275  nbumgr  29279  uhgrnbgr0nb  29286  nbusgrf1o0  29301  uvtxnbgrvtx  29325  cusgrfilem2  29389  uspgr2wlkeq  29578  wwlks  29767  iswwlksnon  29785  rusgr0edg  29905  clwwlkccatlem  29920  clwwisshclwwslem  29945  clwwlkn  29957  clwwlknon  30021  3cyclfrgrrn  30217  vdgn1frgrv3  30228  2wspmdisj  30268  numclwlk2lem2f1o  30310  frgrregord013  30326  htthlem  30848  ocsh  31214  shintcli  31260  pjss2coi  32095  pjnormssi  32099  pjclem4  32130  pj3si  32138  pj3cor1i  32140  strlem3a  32183  strb  32189  hstrlem3a  32191  hstrbi  32197  spansncv2  32224  mdsl1i  32252  cvmdi  32255  mdexchi  32266  h1da  32280  mdsymlem6  32339  sumdmdii  32346  dmdbr5ati  32353  isoun  32635  xrge0tsmsd  33010  ordtrest2NEW  33904  pwsiga  34111  measiun  34199  dya2iocuni  34264  bnj518  34866  bnj1137  34975  bnj1136  34977  bnj1413  35015  bnj1417  35021  bnj60  35042  tz9.1regs  35080  fineqvnttrclselem3  35089  gblacfnacd  35092  onvf1odlem1  35093  onvf1odlem4  35096  subgrwlk  35122  erdszelem8  35188  cvmsss2  35264  cvmfolem  35269  fmlasucdisj  35389  satfun  35401  dfon2lem8  35781  dfon2lem9  35782  dfon2  35783  rdgprc  35785  nn0prpwlem  36313  ntruni  36318  clsint2  36320  fneint  36339  fnessref  36348  refssfne  36349  neibastop1  36350  neibastop2lem  36351  bj-0int  37092  bj-ismooredr  37100  relowlpssretop  37355  fvineqsneu  37402  fvineqsneq  37403  heicant  37652  mblfinlem1  37654  ftc2nc  37699  sdclem2  37739  fdc  37742  seqpo  37744  prdsbnd  37790  heibor  37818  rrnequiv  37832  0idl  38022  intidl  38026  unichnidl  38028  prnc  38064  refressn  38437  lsmcv2  39025  lcvexchlem4  39033  lcvexchlem5  39034  eqlkr  39095  paddclN  39838  pclfinN  39896  ldilcnv  40111  ldilco  40112  cdleme25dN  40352  cdlemj2  40818  tendocan  40820  erng1lem  40983  erngdvlem4-rN  40995  dihord2pre  41221  dihglblem2N  41290  dochvalr  41353  hdmap14lem12  41875  hdmap14lem13  41876  supinf  42232  fsuppind  42580  pellfundre  42871  pellfundge  42872  pellfundlb  42874  dford3lem1  43016  aomclem2  43045  oaabsb  43284  cantnf2  43315  ofoafg  43344  naddcnff  43352  naddwordnexlem3  43389  naddwordnexlem4  43391  pwinfi3  43553  iunrelexp0  43692  iunrelexpmin1  43698  iunrelexpmin2  43702  dftrcl3  43710  cnvtrclfv  43714  trclimalb2  43716  dfrtrcl3  43723  ntrneiel2  44076  ntrneik4w  44090  ntrrn  44112  gneispa  44120  gneispb  44121  addrcom  44464  iunconnlem2  44924  ssuzfz  45345  dvnprodlem3  45943  funressnfv  47041  cfsetsnfsetfo  47058  tz6.12-afv  47171  tz6.12-afv2  47238  otiunsndisjX  47277  uniimaprimaeqfv  47380  iccpartltu  47423  iccpartgtl  47424  iccpartleu  47426  iccpartgel  47427  fargshiftf  47438  fargshiftfva  47441  sbgoldbst  47776  bgoldbtbnd  47807  tgblthelfgott  47813  grimuhgr  47885  grimco  47887  isuspgrim0  47892  isuspgrimlem  47893  upgrimpths  47907  gricushgr  47915  grtriclwlk3  47943  stgr0  47958  uspgrlim  47990  grlicsym  48011  nnsgrp  48175  ellcoellss  48434  lindsrng01  48467  suppdm  48509  nn0sumshdiglem1  48620  setrec2fun  49691