Theorem ralrimiv 3123

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  ralrimiva  3124  ralrimivw  3128  ralrimdv  3130  ralrimivv  3173  rr19.3v  3617  class2seteq  3658  rabssdv  4020  rzalALT  4457  disjord  5078  disjiund  5080  trin  5207  ralxfrALT  5351  otiunsndisj  5458  onmindif  6400  fnprb  7142  fntpb  7143  f1cdmsn  7216  ssorduni  7712  onminex  7735  onmindif2  7740  limuni3  7782  frxp  8056  poxp  8058  sexp2  8076  sexp3  8083  onfununi  8261  onnseq  8264  tfrlem12  8308  tz7.48-2  8361  oaass  8476  omass  8495  oelim2  8510  oelimcl  8515  oaabs2  8564  omabs  8566  uniqs  8698  undifixp  8858  dom2lem  8914  isinf  9149  unblem4  9179  unbnn2  9181  marypha1lem  9317  supssd  9347  supiso  9360  infssd  9378  ordiso2  9401  card2inf  9441  elirrvOLD  9484  wemapwe  9587  ttrclss  9610  trcl  9618  frr3g  9649  tz9.13  9684  rankval3b  9719  rankunb  9743  rankuni2b  9746  scott0  9779  updjud  9827  dfac8alem  9920  carduniima  9987  alephsmo  9993  alephval3  10001  iunfictbso  10005  dfac3  10012  dfac5lem5  10018  dfac12r  10038  dfac12k  10039  kmlem4  10045  kmlem11  10052  cfsuc  10148  cofsmo  10160  cfsmolem  10161  coftr  10164  alephsing  10167  infpssrlem3  10196  fin23lem30  10233  isf32lem2  10245  isf32lem3  10246  isf34lem6  10271  fin1a2lem11  10301  fin1a2lem13  10303  fin1a2s  10305  axcc2lem  10327  domtriomlem  10333  axdc3lem2  10342  axdc4lem  10346  axcclem  10348  axdclem2  10411  iundom2g  10431  uniimadom  10435  cardmin  10455  alephval2  10463  alephreg  10473  fpwwe2lem11  10532  wunex2  10629  wuncval2  10638  tskwe2  10664  inar1  10666  tskuni  10674  gruun  10697  intgru  10705  grutsk1  10712  genpcl  10899  ltexprlem5  10931  suplem1pr  10943  supexpr  10945  supsrlem  11002  axpre-sup  11060  negfi  12071  supaddc  12089  supadd  12090  supmul1  12091  supmullem1  12092  supmul  12094  peano5nni  12128  uzind  12565  zindd  12574  uzwo  12809  lbzbi  12834  xrsupsslem  13206  xrinfmsslem  13207  supxrun  13215  supxrpnf  13217  supxrunb1  13218  supxrunb2  13219  icoshftf1o  13374  flval3  13719  axdc4uzlem  13890  tpfo  14407  wrdnfi  14455  ccatrn  14497  ccatalpha  14501  2cshw  14720  cshweqrep  14728  s3iunsndisj  14875  rtrclreclem4  14968  dfrtrcl2  14969  01sqrexlem1  15149  01sqrexlem6  15154  fsum0diag2  15690  alzdvds  16231  gcdcllem1  16410  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  maxprmfct  16620  hashgcdeq  16701  unbenlem  16820  vdwlem6  16898  vdwlem10  16902  firest  17336  mrieqv2d  17545  iscatd  17579  initoeu2  17923  setcmon  17994  setcepi  17995  fullestrcsetc  18057  fullsetcestrc  18072  isglbd  18415  isacs4lem  18450  acsfiindd  18459  acsmapd  18460  psss  18486  sgrpidmnd  18647  pwmnd  18845  ghmrn  19141  ghmpreima  19150  cntz2ss  19247  symgextres  19337  psgnunilem2  19407  lsmsubg  19566  efgsfo  19651  gsumzaddlem  19833  gsummptnn0fzfv  19899  dmdprdd  19913  dprd2da  19956  ablsimpgprmd  20029  imasring  20248  01eq0ring  20445  isabvd  20727  issrngd  20770  islssd  20868  lbsextlem3  21097  lbsextlem4  21098  lidldvgen  21271  pzriprnglem4  21421  pzriprnglem7  21424  pzriprnglem13  21430  psgnghm  21517  isphld  21591  frlmsslsp  21733  mp2pm2mplem4  22724  tgcl  22884  distop  22910  indistopon  22916  pptbas  22923  toponmre  23008  opnnei  23035  neiuni  23037  neindisj2  23038  ordtrest2  23119  cnpnei  23179  cnindis  23207  cmpcld  23317  uncmp  23318  hauscmplem  23321  2ndc1stc  23366  1stcrest  23368  1stcelcls  23376  llyrest  23400  nllyrest  23401  cldllycmp  23410  reftr  23429  locfincf  23446  comppfsc  23447  txcls  23519  ptpjcn  23526  ptclsg  23530  dfac14lem  23532  xkoccn  23534  txlly  23551  txnlly  23552  ptrescn  23554  tx1stc  23565  xkoco1cn  23572  xkoco2cn  23573  xkococn  23575  xkoinjcn  23602  qtopeu  23631  hmeofval  23673  ordthmeolem  23716  isfild  23773  fbasrn  23799  trfil2  23802  flimclslem  23899  fclsrest  23939  fclscf  23940  flimfcls  23941  alexsubALTlem1  23962  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALT  23966  qustgpopn  24035  isxmetd  24241  imasdsf1olem  24288  blcls  24421  prdsxmslem2  24444  metustfbas  24472  dscmet  24487  nrmmetd  24489  reperflem  24734  reconnlem2  24743  xrge0tsms  24750  fsumcn  24788  cnheibor  24881  tcphcph  25164  lmmbr  25185  caubl  25235  ivthlem1  25379  ovolctb  25418  ovoliunlem2  25431  ovolscalem1  25441  ovolicc2  25450  voliunlem3  25480  ismbfd  25567  mbfimaopnlem  25583  itg2le  25667  ellimc2  25805  c1liplem1  25928  plyeq0lem  26142  dgreq0  26198  aannenlem1  26263  pilem2  26389  cxpcn3lem  26684  scvxcvx  26923  musum  27128  fsumdvdsmul  27132  dchrisum0flb  27448  ostth2lem2  27572  sltval2  27595  nolesgn2ores  27611  nogesgn1ores  27613  nosupres  27646  nosupbnd2lem1  27654  noinfres  27661  noinfbnd2lem1  27669  scutun12  27751  madebdayim  27833  precsexlem9  28153  noseqind  28222  zs12zodd  28392  zs12bday  28394  numedglnl  29122  upgrreslem  29282  umgrreslem  29283  nbuhgr  29321  nbumgr  29325  uhgrnbgr0nb  29332  nbusgrf1o0  29347  uvtxnbgrvtx  29371  cusgrfilem2  29435  uspgr2wlkeq  29624  wwlks  29813  iswwlksnon  29831  rusgr0edg  29954  clwwlkccatlem  29969  clwwisshclwwslem  29994  clwwlkn  30006  clwwlknon  30070  3cyclfrgrrn  30266  vdgn1frgrv3  30277  2wspmdisj  30317  numclwlk2lem2f1o  30359  frgrregord013  30375  htthlem  30897  ocsh  31263  shintcli  31309  pjss2coi  32144  pjnormssi  32148  pjclem4  32179  pj3si  32187  pj3cor1i  32189  strlem3a  32232  strb  32238  hstrlem3a  32240  hstrbi  32246  spansncv2  32273  mdsl1i  32301  cvmdi  32304  mdexchi  32315  h1da  32329  mdsymlem6  32388  sumdmdii  32395  dmdbr5ati  32402  isoun  32683  xrge0tsmsd  33042  ordtrest2NEW  33936  pwsiga  34143  measiun  34231  dya2iocuni  34296  bnj518  34898  bnj1137  35007  bnj1136  35009  bnj1413  35047  bnj1417  35053  bnj60  35074  rankval4b  35111  r1filim  35115  trssfir1om  35122  tz9.1regs  35130  trssfir1omregs  35132  fineqvnttrclselem3  35143  gblacfnacd  35146  onvf1odlem1  35147  onvf1odlem4  35150  subgrwlk  35176  erdszelem8  35242  cvmsss2  35318  cvmfolem  35323  fmlasucdisj  35443  satfun  35455  dfon2lem8  35832  dfon2lem9  35833  dfon2  35834  rdgprc  35836  nn0prpwlem  36366  ntruni  36371  clsint2  36373  fneint  36392  fnessref  36401  refssfne  36402  neibastop1  36403  neibastop2lem  36404  bj-0int  37145  bj-ismooredr  37153  relowlpssretop  37408  fvineqsneu  37455  fvineqsneq  37456  heicant  37694  mblfinlem1  37696  ftc2nc  37741  sdclem2  37781  fdc  37784  seqpo  37786  prdsbnd  37832  heibor  37860  rrnequiv  37874  0idl  38064  intidl  38068  unichnidl  38070  prnc  38106  refressn  38544  lsmcv2  39127  lcvexchlem4  39135  lcvexchlem5  39136  eqlkr  39197  paddclN  39940  pclfinN  39998  ldilcnv  40213  ldilco  40214  cdleme25dN  40454  cdlemj2  40920  tendocan  40922  erng1lem  41085  erngdvlem4-rN  41097  dihord2pre  41323  dihglblem2N  41392  dochvalr  41455  hdmap14lem12  41977  hdmap14lem13  41978  supinf  42334  fsuppind  42682  pellfundre  42973  pellfundge  42974  pellfundlb  42976  dford3lem1  43118  aomclem2  43147  oaabsb  43386  cantnf2  43417  ofoafg  43446  naddcnff  43454  naddwordnexlem3  43491  naddwordnexlem4  43493  pwinfi3  43655  iunrelexp0  43794  iunrelexpmin1  43800  iunrelexpmin2  43804  dftrcl3  43812  cnvtrclfv  43816  trclimalb2  43818  dfrtrcl3  43825  ntrneiel2  44178  ntrneik4w  44192  ntrrn  44214  gneispa  44222  gneispb  44223  addrcom  44566  iunconnlem2  45026  ssuzfz  45447  dvnprodlem3  46045  funressnfv  47142  cfsetsnfsetfo  47159  tz6.12-afv  47272  tz6.12-afv2  47339  otiunsndisjX  47378  uniimaprimaeqfv  47481  iccpartltu  47524  iccpartgtl  47525  iccpartleu  47527  iccpartgel  47528  fargshiftf  47539  fargshiftfva  47542  sbgoldbst  47877  bgoldbtbnd  47908  tgblthelfgott  47914  grimuhgr  47986  grimco  47988  isuspgrim0  47993  isuspgrimlem  47994  upgrimpths  48008  gricushgr  48016  grtriclwlk3  48044  stgr0  48059  uspgrlim  48091  grlicsym  48112  nnsgrp  48276  ellcoellss  48535  lindsrng01  48568  suppdm  48610  nn0sumshdiglem1  48721  setrec2fun  49792