Theorem ralrimiv 3126

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 1912	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ralrimiv.1	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	hbralrimi 3125	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3050

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

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

This theorem is referenced by:  ralrimiva  3127  ralrimivw  3131  ralrimdv  3133  ralrimivv  3176  rr19.3v  3620  class2seteq  3661  rabssdv  4025  rzalALT  4447  r19.3rzv  4455  disjord  5086  disjiund  5088  trin  5215  ralxfrALT  5359  otiunsndisj  5467  onmindif  6410  fnprb  7154  fntpb  7155  f1cdmsn  7228  ssorduni  7724  onminex  7747  onmindif2  7752  limuni3  7794  frxp  8068  poxp  8070  sexp2  8088  sexp3  8095  onfununi  8273  onnseq  8276  tfrlem12  8320  tz7.48-2  8373  oaass  8488  omass  8507  oelim2  8523  oelimcl  8528  oaabs2  8577  omabs  8579  uniqs  8712  undifixp  8874  dom2lem  8931  isinf  9167  unblem4  9197  unbnn2  9199  marypha1lem  9338  supssd  9368  supiso  9381  infssd  9399  ordiso2  9422  card2inf  9462  elirrvOLD  9505  wemapwe  9608  ttrclss  9631  trcl  9639  frr3g  9670  tz9.13  9705  rankval3b  9740  rankunb  9764  rankuni2b  9767  scott0  9800  updjud  9848  dfac8alem  9941  carduniima  10008  alephsmo  10014  alephval3  10022  iunfictbso  10026  dfac3  10033  dfac5lem5  10039  dfac12r  10059  dfac12k  10060  kmlem4  10066  kmlem11  10073  cfsuc  10169  cofsmo  10181  cfsmolem  10182  coftr  10185  alephsing  10188  infpssrlem3  10217  fin23lem30  10254  isf32lem2  10266  isf32lem3  10267  isf34lem6  10292  fin1a2lem11  10322  fin1a2lem13  10324  fin1a2s  10326  axcc2lem  10348  domtriomlem  10354  axdc3lem2  10363  axdc4lem  10367  axcclem  10369  axdclem2  10432  iundom2g  10452  uniimadom  10456  cardmin  10476  alephval2  10485  alephreg  10495  fpwwe2lem11  10554  wunex2  10651  wuncval2  10660  tskwe2  10686  inar1  10688  tskuni  10696  gruun  10719  intgru  10727  grutsk1  10734  genpcl  10921  ltexprlem5  10953  suplem1pr  10965  supexpr  10967  supsrlem  11024  axpre-sup  11082  negfi  12093  supaddc  12111  supadd  12112  supmul1  12113  supmullem1  12114  supmul  12116  peano5nni  12150  uzind  12586  zindd  12595  uzwo  12826  lbzbi  12851  xrsupsslem  13224  xrinfmsslem  13225  supxrun  13233  supxrpnf  13235  supxrunb1  13236  supxrunb2  13237  icoshftf1o  13392  flval3  13737  axdc4uzlem  13908  tpfo  14425  wrdnfi  14473  ccatrn  14515  ccatalpha  14519  2cshw  14738  cshweqrep  14746  s3iunsndisj  14893  rtrclreclem4  14986  dfrtrcl2  14987  01sqrexlem1  15167  01sqrexlem6  15172  fsum0diag2  15708  alzdvds  16249  gcdcllem1  16428  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  maxprmfct  16638  hashgcdeq  16719  unbenlem  16838  vdwlem6  16916  vdwlem10  16920  firest  17354  mrieqv2d  17564  iscatd  17598  initoeu2  17942  setcmon  18013  setcepi  18014  fullestrcsetc  18076  fullsetcestrc  18091  isglbd  18434  isacs4lem  18469  acsfiindd  18478  acsmapd  18479  psss  18505  sgrpidmnd  18666  pwmnd  18864  ghmrn  19160  ghmpreima  19169  cntz2ss  19266  symgextres  19356  psgnunilem2  19426  lsmsubg  19585  efgsfo  19670  gsumzaddlem  19852  gsummptnn0fzfv  19918  dmdprdd  19932  dprd2da  19975  ablsimpgprmd  20048  imasring  20268  01eq0ring  20465  isabvd  20747  issrngd  20790  islssd  20888  lbsextlem3  21117  lbsextlem4  21118  lidldvgen  21291  pzriprnglem4  21441  pzriprnglem7  21444  pzriprnglem13  21450  psgnghm  21537  isphld  21611  frlmsslsp  21753  mp2pm2mplem4  22755  tgcl  22915  distop  22941  indistopon  22947  pptbas  22954  toponmre  23039  opnnei  23066  neiuni  23068  neindisj2  23069  ordtrest2  23150  cnpnei  23210  cnindis  23238  cmpcld  23348  uncmp  23349  hauscmplem  23352  2ndc1stc  23397  1stcrest  23399  1stcelcls  23407  llyrest  23431  nllyrest  23432  cldllycmp  23441  reftr  23460  locfincf  23477  comppfsc  23478  txcls  23550  ptpjcn  23557  ptclsg  23561  dfac14lem  23563  xkoccn  23565  txlly  23582  txnlly  23583  ptrescn  23585  tx1stc  23596  xkoco1cn  23603  xkoco2cn  23604  xkococn  23606  xkoinjcn  23633  qtopeu  23662  hmeofval  23704  ordthmeolem  23747  isfild  23804  fbasrn  23830  trfil2  23833  flimclslem  23930  fclsrest  23970  fclscf  23971  flimfcls  23972  alexsubALTlem1  23993  alexsubALTlem2  23994  alexsubALTlem3  23995  alexsubALT  23997  qustgpopn  24066  isxmetd  24272  imasdsf1olem  24319  blcls  24452  prdsxmslem2  24475  metustfbas  24503  dscmet  24518  nrmmetd  24520  reperflem  24765  reconnlem2  24774  xrge0tsms  24781  fsumcn  24819  cnheibor  24912  tcphcph  25195  lmmbr  25216  caubl  25266  ivthlem1  25410  ovolctb  25449  ovoliunlem2  25462  ovolscalem1  25472  ovolicc2  25481  voliunlem3  25511  ismbfd  25598  mbfimaopnlem  25614  itg2le  25698  ellimc2  25836  c1liplem1  25959  plyeq0lem  26173  dgreq0  26229  aannenlem1  26294  pilem2  26420  cxpcn3lem  26715  scvxcvx  26954  musum  27159  fsumdvdsmul  27163  dchrisum0flb  27479  ostth2lem2  27603  sltval2  27626  nolesgn2ores  27642  nogesgn1ores  27644  nosupres  27677  nosupbnd2lem1  27685  noinfres  27692  noinfbnd2lem1  27700  scutun12  27786  madebdayim  27868  precsexlem9  28194  addsonbday  28258  noseqind  28271  zs12zodd  28459  numedglnl  29198  upgrreslem  29358  umgrreslem  29359  nbuhgr  29397  nbumgr  29401  uhgrnbgr0nb  29408  nbusgrf1o0  29423  uvtxnbgrvtx  29447  cusgrfilem2  29511  uspgr2wlkeq  29700  wwlks  29889  iswwlksnon  29907  rusgr0edg  30030  clwwlkccatlem  30045  clwwisshclwwslem  30070  clwwlkn  30082  clwwlknon  30146  3cyclfrgrrn  30342  vdgn1frgrv3  30353  2wspmdisj  30393  numclwlk2lem2f1o  30435  frgrregord013  30451  htthlem  30973  ocsh  31339  shintcli  31385  pjss2coi  32220  pjnormssi  32224  pjclem4  32255  pj3si  32263  pj3cor1i  32265  strlem3a  32308  strb  32314  hstrlem3a  32316  hstrbi  32322  spansncv2  32349  mdsl1i  32377  cvmdi  32380  mdexchi  32391  h1da  32405  mdsymlem6  32464  sumdmdii  32471  dmdbr5ati  32478  isoun  32760  xrge0tsmsd  33134  ordtrest2NEW  34059  pwsiga  34266  measiun  34354  dya2iocuni  34419  bnj518  35021  bnj1137  35130  bnj1136  35132  bnj1413  35170  bnj1417  35176  bnj60  35197  rankval4b  35235  r1filim  35239  trssfir1om  35246  fineqvnttrclselem3  35258  fineqvinfep  35260  tz9.1regs  35269  trssfir1omregs  35271  gblacfnacd  35275  onvf1odlem1  35276  onvf1odlem4  35279  subgrwlk  35305  erdszelem8  35371  cvmsss2  35447  cvmfolem  35452  fmlasucdisj  35572  satfun  35584  dfon2lem8  35961  dfon2lem9  35962  dfon2  35963  rdgprc  35965  nn0prpwlem  36495  ntruni  36500  clsint2  36502  fneint  36521  fnessref  36530  refssfne  36531  neibastop1  36532  neibastop2lem  36533  bj-0int  37275  bj-ismooredr  37283  relowlpssretop  37538  fvineqsneu  37585  fvineqsneq  37586  heicant  37825  mblfinlem1  37827  ftc2nc  37872  sdclem2  37912  fdc  37915  seqpo  37917  prdsbnd  37963  heibor  37991  rrnequiv  38005  0idl  38195  intidl  38199  unichnidl  38201  prnc  38237  refressn  38703  lsmcv2  39324  lcvexchlem4  39332  lcvexchlem5  39333  eqlkr  39394  paddclN  40137  pclfinN  40195  ldilcnv  40410  ldilco  40411  cdleme25dN  40651  cdlemj2  41117  tendocan  41119  erng1lem  41282  erngdvlem4-rN  41294  dihord2pre  41520  dihglblem2N  41589  dochvalr  41652  hdmap14lem12  42174  hdmap14lem13  42175  supinf  42534  fsuppind  42870  pellfundre  43160  pellfundge  43161  pellfundlb  43163  dford3lem1  43305  aomclem2  43334  oaabsb  43573  cantnf2  43604  ofoafg  43633  naddcnff  43641  naddwordnexlem3  43678  naddwordnexlem4  43680  pwinfi3  43841  iunrelexp0  43980  iunrelexpmin1  43986  iunrelexpmin2  43990  dftrcl3  43998  cnvtrclfv  44002  trclimalb2  44004  dfrtrcl3  44011  ntrneiel2  44364  ntrneik4w  44378  ntrrn  44400  gneispa  44408  gneispb  44409  addrcom  44752  iunconnlem2  45212  ssuzfz  45631  dvnprodlem3  46229  funressnfv  47326  cfsetsnfsetfo  47343  tz6.12-afv  47456  tz6.12-afv2  47523  otiunsndisjX  47562  uniimaprimaeqfv  47665  iccpartltu  47708  iccpartgtl  47709  iccpartleu  47711  iccpartgel  47712  fargshiftf  47723  fargshiftfva  47726  sbgoldbst  48061  bgoldbtbnd  48092  tgblthelfgott  48098  grimuhgr  48170  grimco  48172  isuspgrim0  48177  isuspgrimlem  48178  upgrimpths  48192  gricushgr  48200  grtriclwlk3  48228  stgr0  48243  uspgrlim  48275  grlicsym  48296  nnsgrp  48460  ellcoellss  48718  lindsrng01  48751  suppdm  48793  nn0sumshdiglem1  48904  setrec2fun  49974