Theorem ralrimiv 3155

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

Syntax hints:   → wi 4   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-ral 3079

This theorem is referenced by:  ralrimiva  3156  ralrimivw  3160  ralrimdv  3162  ralrimivv  3205  rr19.3v  3628  class2seteq  3669  rabssdv  4029  rzalALT  4451  r19.3rzv  4459  disjord  5091  disjiund  5093  trun  5220  trin  5221  ralxfrALT  5374  otiunsndisj  5491  onmindif  6442  fnprb  7194  fntpb  7195  f1cdmsn  7268  ssorduni  7764  onminex  7787  onmindif2  7792  limuni3  7834  frxp  8108  poxp  8110  sexp2  8128  sexp3  8135  onfununi  8314  onnseq  8317  tfrlem12  8362  tz7.48-2  8415  oaass  8532  omass  8551  oelim2  8567  oelimcl  8572  oaabs2  8621  omabs  8623  uniqs  8757  undifixp  8918  dom2lem  8975  isinf  9211  unblem4  9241  unbnn2  9243  marypha1lem  9381  supssd  9411  supiso  9424  infssd  9442  ordiso2  9465  card2inf  9505  elirrvOLDOLD  9549  wemapwe  9654  ttrclss  9677  trcl  9685  frr3g  9716  tz9.13  9751  rankval3b  9786  rankunb  9810  rankuni2b  9813  scott0  9846  updjud  9894  dfac8alem  9987  carduniima  10054  alephsmo  10060  alephval3  10068  iunfictbso  10072  dfac3  10079  dfac5lem5  10085  dfac12r  10105  dfac12k  10106  kmlem4  10112  kmlem11  10119  cfsuc  10216  cofsmo  10228  cfsmolem  10229  coftr  10232  alephsing  10235  infpssrlem3  10264  fin23lem30  10301  isf32lem2  10313  isf32lem3  10314  isf34lem6  10339  fin1a2lem11  10369  fin1a2lem13  10371  fin1a2s  10373  axcc2lem  10395  domtriomlem  10401  axdc3lem2  10410  axdc4lem  10414  axcclem  10416  axdclem2  10479  iundom2g  10499  uniimadom  10503  cardmin  10523  alephval2  10532  alephreg  10542  fpwwe2lem11  10601  wunex2  10698  wuncval2  10707  tskwe2  10733  inar1  10735  tskuni  10743  gruun  10766  intgru  10774  grutsk1  10781  genpcl  10968  ltexprlem5  11000  suplem1pr  11012  supexpr  11014  supsrlem  11071  axpre-sup  11129  negfi  12143  supaddc  12161  supadd  12162  supmul1  12163  supmullem1  12164  supmul  12166  peano5nni  12215  uzind  12667  zindd  12676  uzwo  12914  lbzbi  12939  xrsupsslem  13312  xrinfmsslem  13313  supxrun  13321  supxrpnf  13323  supxrunb1  13324  supxrunb2  13325  icoshftf1o  13480  flval3  13827  axdc4uzlem  13998  tpfo  14515  wrdnfi  14563  ccatrn  14605  ccatalpha  14609  2cshw  14828  cshweqrep  14836  s3iunsndisj  14983  rtrclreclem4  15076  dfrtrcl2  15077  01sqrexlem1  15271  01sqrexlem6  15276  fsum0diag2  15812  alzdvds  16356  gcdcllem1  16535  lcmfunsnlem2lem1  16674  lcmfunsnlem2lem2  16675  maxprmfct  16746  hashgcdeq  16827  unbenlem  16946  vdwlem6  17024  vdwlem10  17028  firest  17463  mrieqv2d  17673  iscatd  17707  initoeu2  18051  setcmon  18122  setcepi  18123  fullestrcsetc  18185  fullsetcestrc  18200  isglbd  18543  isacs4lem  18578  acsfiindd  18587  acsmapd  18588  psss  18614  sgrpidmnd  18775  pwmnd  18976  ghmrn  19271  ghmpreima  19280  cntz2ss  19377  symgextres  19467  psgnunilem2  19537  lsmsubg  19696  efgsfo  19781  gsumzaddlem  19963  gsummptnn0fzfv  20029  dmdprdd  20043  dprd2da  20086  ablsimpgprmd  20159  imasring  20381  01eq0ring  20582  isabvd  20863  issrngd  20906  islssd  21004  lbsextlem3  21232  lbsextlem4  21233  lidldvgen  21406  pzriprnglem4  21538  pzriprnglem7  21541  pzriprnglem13  21547  psgnghm  21634  isphld  21708  frlmsslsp  21850  mp2pm2mplem4  22871  tgcl  23031  distop  23057  indistopon  23063  pptbas  23070  toponmre  23155  opnnei  23182  neiuni  23184  neindisj2  23185  ordtrest2  23266  cnpnei  23326  cnindis  23354  cmpcld  23464  uncmp  23465  hauscmplem  23468  2ndc1stc  23513  1stcrest  23515  1stcelcls  23523  llyrest  23547  nllyrest  23548  cldllycmp  23557  reftr  23576  locfincf  23593  comppfsc  23594  txcls  23666  ptpjcn  23673  ptclsg  23677  dfac14lem  23679  xkoccn  23681  txlly  23698  txnlly  23699  ptrescn  23701  tx1stc  23712  xkoco1cn  23719  xkoco2cn  23720  xkococn  23722  xkoinjcn  23749  qtopeu  23778  hmeofval  23820  ordthmeolem  23863  isfild  23920  fbasrn  23946  trfil2  23949  flimclslem  24046  fclsrest  24086  fclscf  24087  flimfcls  24088  alexsubALTlem1  24109  alexsubALTlem2  24110  alexsubALTlem3  24111  alexsubALT  24113  qustgpopn  24182  isxmetd  24388  imasdsf1olem  24435  blcls  24568  prdsxmslem2  24591  metustfbas  24619  dscmet  24634  nrmmetd  24636  reperflem  24881  reconnlem2  24890  xrge0tsms  24897  fsumcn  24934  cnheibor  25019  tcphcph  25301  lmmbr  25322  caubl  25372  ivthlem1  25515  ovolctb  25554  ovoliunlem2  25567  ovolscalem1  25577  ovolicc2  25586  voliunlem3  25616  ismbfd  25703  mbfimaopnlem  25719  itg2le  25803  ellimc2  25941  c1liplem1  26060  plyeq0lem  26272  dgreq0  26327  aannenlem1  26394  pilem2  26517  cxpcn3lem  26814  scvxcvx  27052  musum  27257  fsumdvdsmul  27261  dchrisum0flb  27576  ostth2lem2  27700  ltsval2  27722  nolesgn2ores  27738  nogesgn1ores  27740  nosupres  27773  nosupbnd2lem1  27781  noinfres  27788  noinfbnd2lem1  27796  cutsun12  27885  madebdayim  27983  precsexlem9  28310  addonbday  28374  noseqind  28387  z12zsodd  28577  numedglnl  29347  upgrreslem  29507  umgrreslem  29508  nbuhgr  29546  nbumgr  29550  uhgrnbgr0nb  29557  nbusgrf1o0  29572  uvtxnbgrvtx  29596  cusgrfilem2  29659  uspgr2wlkeq  29848  wwlks  30037  iswwlksnon  30055  rusgr0edg  30178  clwwlkccatlem  30193  clwwisshclwwslem  30218  clwwlkn  30230  clwwlknon  30294  3cyclfrgrrn  30490  vdgn1frgrv3  30501  2wspmdisj  30541  numclwlk2lem2f1o  30583  frgrregord013  30599  htthlem  31122  ocsh  31488  shintcli  31534  pjss2coi  32369  pjnormssi  32373  pjclem4  32404  pj3si  32412  pj3cor1i  32414  strlem3a  32457  strb  32463  hstrlem3a  32465  hstrbi  32471  spansncv2  32498  mdsl1i  32526  cvmdi  32529  mdexchi  32540  h1da  32554  mdsymlem6  32613  sumdmdii  32620  dmdbr5ati  32627  isoun  32906  xrge0tsmsd  33255  ordtrest2NEW  34222  pwsiga  34429  measiun  34517  dya2iocuni  34582  bnj518  35183  bnj1137  35292  bnj1136  35294  bnj1413  35332  bnj1417  35338  bnj60  35359  rankval4b  35400  r1filim  35404  trssfir1om  35411  fineqvnttrclselem3  35423  fineqvinfep  35425  tz9.1regs  35434  trssfir1omregs  35436  gblacfnacd  35449  onvf1odlem1  35450  onvf1odlem4  35453  vonf1oonfo  35462  subgrwlk  35487  erdszelem8  35553  cvmsss2  35629  cvmfolem  35634  fmlasucdisj  35754  satfun  35766  dfon2lem8  36143  dfon2lem9  36144  dfon2  36145  rdgprc  36147  nn0prpwlem  36687  ntruni  36692  clsint2  36694  fneint  36713  fnessref  36722  refssfne  36723  neibastop1  36724  neibastop2lem  36725  mh-inf3f1  36906  bj-0int  37596  bj-ismooredr  37604  relowlpssretop  37863  fvineqsneu  37910  fvineqsneq  37911  heicant  38159  mblfinlem1  38161  ftc2nc  38206  sdclem2  38246  fdc  38249  seqpo  38251  prdsbnd  38297  heibor  38325  rrnequiv  38339  0idl  38529  intidl  38533  unichnidl  38535  prnc  38571  refressn  39037  lsmcv2  39658  lcvexchlem4  39666  lcvexchlem5  39667  eqlkr  39728  paddclN  40471  pclfinN  40529  ldilcnv  40744  ldilco  40745  cdleme25dN  40985  cdlemj2  41451  tendocan  41453  erng1lem  41616  erngdvlem4-rN  41628  dihord2pre  41854  dihglblem2N  41923  dochvalr  41986  hdmap14lem12  42508  hdmap14lem13  42509  supinf  42863  fsuppind  43177  pellfundre  43463  pellfundge  43464  pellfundlb  43466  dford3lem1  43608  aomclem2  43637  oaabsb  43876  cantnf2  43907  ofoafg  43936  naddcnff  43944  naddwordnexlem3  43981  naddwordnexlem4  43983  pwinfi3  44144  iunrelexp0  44283  iunrelexpmin1  44289  iunrelexpmin2  44293  dftrcl3  44301  cnvtrclfv  44305  trclimalb2  44307  dfrtrcl3  44314  ntrneiel2  44667  ntrneik4w  44681  ntrrn  44703  gneispa  44711  gneispb  44712  addrcom  45055  iunconnlem2  45515  ssuzfz  45930  dvnprodlem3  46527  funressnfv  47642  cfsetsnfsetfo  47659  tz6.12-afv  47772  tz6.12-afv2  47839  otiunsndisjX  47878  uniimaprimaeqfv  47993  iccpartltu  48036  iccpartgtl  48037  iccpartleu  48039  iccpartgel  48040  fargshiftf  48051  fargshiftfva  48054  sbgoldbst  48405  bgoldbtbnd  48436  tgblthelfgott  48442  grimuhgr  48514  grimco  48516  isuspgrim0  48521  isuspgrimlem  48522  upgrimpths  48536  gricushgr  48544  grtriclwlk3  48572  stgr0  48587  uspgrlim  48619  grlicsym  48640  nnsgrp  48804  ellcoellss  49062  lindsrng01  49095  suppdm  49137  nn0sumshdiglem1  49248  setrec2fun  50318