Theorem ralrimiv 3153

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  ralrimiva  3154  ralrimivw  3158  ralrimdv  3160  ralrimivv  3203  rr19.3v  3621  class2seteq  3662  rabssdv  4022  rzalALT  4451  r19.3rzv  4459  disjord  5092  disjiund  5094  trun  5223  trin  5224  ralxfrALT  5380  otiunsndisj  5497  onmindif  6452  fnprb  7207  fntpb  7208  f1cdmsn  7283  ssorduni  7778  onminex  7801  onmindif2  7806  limuni3  7848  frxp  8124  poxp  8126  sexp2  8144  sexp3  8151  onfununi  8330  onnseq  8333  tfrlem12  8378  tz7.48-2  8431  oaass  8548  omass  8567  oelim2  8583  oelimcl  8588  oaabs2  8637  omabs  8639  uniqs  8773  undifixp  8941  dom2lem  8998  isinf  9235  unblem4  9265  unbnn2  9267  marypha1lem  9403  supssd  9433  supiso  9446  infssd  9464  ordiso2  9487  card2inf  9527  elirrvOLDOLD  9571  wemapwe  9676  ttrclss  9699  trcl  9707  frr3g  9738  tz9.13  9773  rankval3b  9808  rankunb  9832  rankuni2b  9835  scott0b  9876  scott0OLD  9877  updjud  9939  dfac8alem  10032  carduniima  10099  alephsmo  10105  alephval3  10113  iunfictbso  10117  dfac3  10124  dfac5lem5  10130  dfac12r  10149  dfac12k  10150  kmlem4  10156  kmlem11  10163  cfsuc  10259  cofsmo  10271  cfsmolem  10272  coftr  10275  alephsing  10278  infpssrlem3  10307  fin23lem30  10344  isf32lem2  10356  isf32lem3  10357  isf34lem6  10382  fin1a2lem11  10412  fin1a2lem13  10414  fin1a2s  10416  axcc2lem  10438  domtriomlem  10444  axdc3lem2  10453  axdc4lem  10457  axcclem  10459  axdclem2  10522  iundom2g  10548  uniimadom  10552  cardmin  10572  alephval2  10581  alephreg  10591  fpwwe2lem11  10650  wunex2  10747  wuncval2  10756  tskwe2  10782  inar1  10784  tskuni  10792  gruun  10815  intgru  10823  grutsk1  10830  genpcl  11017  ltexprlem5  11049  suplem1pr  11061  supexpr  11063  supsrlem  11120  axpre-sup  11178  negfi  12188  supaddc  12206  supadd  12207  supmul1  12208  supmullem1  12209  supmul  12211  peano5nni  12260  uzind  12713  zindd  12722  uzwo  12960  lbzbi  12985  xrsupsslem  13359  xrinfmsslem  13360  supxrun  13368  supxrpnf  13370  supxrunb1  13371  supxrunb2  13372  icoshftf1o  13527  flval3  13876  axdc4uzlem  14047  tpfo  14565  wrdnfi  14613  ccatrn  14655  ccatalpha  14660  2cshw  14884  cshweqrep  14892  s3iunsndisj  15041  rtrclreclem4  15134  dfrtrcl2  15135  01sqrexlem1  15329  01sqrexlem6  15334  fsum0diag2  15869  alzdvds  16410  gcdcllem1  16589  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  maxprmfct  16800  hashgcdeq  16881  unbenlem  17000  vdwlem6  17078  vdwlem10  17082  firest  17517  mrieqv2d  17727  iscatd  17761  initoeu2  18105  setcmon  18176  setcepi  18177  fullestrcsetc  18239  fullsetcestrc  18254  isglbd  18597  isacs4lem  18632  acsfiindd  18641  acsmapd  18642  psss  18668  mgmn0plusgf  18741  sgrpidmnd  18841  pwmnd  19056  ghmrn  19356  ghmpreima  19365  cntz2ss  19462  symgextres  19552  psgnunilem2  19622  lsmsubg  19781  efgsfo  19866  gsumzaddlem  20048  gsummptnn0fzfv  20114  dmdprdd  20128  dprd2da  20171  ablsimpgprmd  20244  imasring  20471  01eq0ring  20691  isabvd  20978  issrngd  21021  islssd  21119  lbsextlem3  21347  lbsextlem4  21348  unichnlidl  21425  lidldvgen  21565  pzriprnglem4  21697  pzriprnglem7  21700  pzriprnglem13  21706  psgnghm  21793  isphld  21867  frlmsslsp  22009  mp2pm2mplem4  23034  tgcl  23194  distop  23220  indistopon  23226  pptbas  23233  toponmre  23318  opnnei  23345  neiuni  23347  neindisj2  23348  ordtrest2  23429  cnpnei  23489  cnindis  23517  cmpcld  23627  uncmp  23628  hauscmplem  23631  2ndc1stc  23676  1stcrest  23678  1stcelcls  23687  llyrest  23711  nllyrest  23712  cldllycmp  23721  reftr  23740  locfincf  23757  comppfsc  23758  txcls  23830  ptpjcn  23837  ptclsg  23841  dfac14lem  23843  xkoccn  23845  txlly  23862  txnlly  23863  ptrescn  23865  tx1stc  23876  xkoco1cn  23883  xkoco2cn  23884  xkococn  23886  xkoinjcn  23913  qtopeu  23942  hmeofval  23984  ordthmeolem  24027  isfild  24084  fbasrn  24110  trfil2  24113  flimclslem  24210  fclsrest  24250  fclscf  24251  flimfcls  24252  alexsubALTlem1  24273  alexsubALTlem2  24274  alexsubALTlem3  24275  alexsubALT  24277  qustgpopn  24346  isxmetd  24552  imasdsf1olem  24599  blcls  24732  prdsxmslem2  24755  metustfbas  24783  dscmet  24798  nrmmetd  24800  reperflem  25045  reconnlem2  25054  xrge0tsms  25061  fsumcn  25098  cnheibor  25183  tcphcph  25465  lmmbr  25486  caubl  25536  ivthlem1  25679  ovolctb  25718  ovoliunlem2  25731  ovolscalem1  25741  ovolicc2  25750  voliunlem3  25780  ismbfd  25867  mbfimaopnlem  25883  itg2le  25967  ellimc2  26104  c1liplem1  26223  plyeq0lem  26436  dgreq0  26491  aannenlem1  26564  pilem2  26688  cxpcn3lem  26984  scvxcvx  27222  musum  27427  fsumdvdsmul  27431  dchrisum0flb  27746  ostth2lem2  27870  ltsval2  27892  nolesgn2ores  27908  nogesgn1ores  27910  nosupres  27943  nosupbnd2lem1  27951  noinfres  27958  noinfbnd2lem1  27966  cutsun12  28055  madebdayim  28153  precsexlem9  28480  addonbday  28544  noseqind  28557  z12zsodd  28747  numedglnl  29601  upgrreslem  29764  umgrreslem  29765  nbuhgr  29803  nbumgr  29807  uhgrnbgr0nb  29814  nbusgrf1o0  29829  uvtxnbgrvtx  29853  cusgrfilem2  29916  uspgr2wlkeq  30105  subgrwlk  30148  wwlks  30303  iswwlksnon  30321  rusgr0edg  30444  clwwlkccatlem  30459  clwwisshclwwslem  30484  clwwlkn  30496  clwwlknon  30560  3cyclfrgrrn  30766  vdgn1frgrv3  30777  2wspmdisj  30817  numclwlk2lem2f1o  30859  frgrregord013  30875  htthlem  31398  ocsh  31764  shintcli  31810  pjss2coi  32645  pjnormssi  32649  pjclem4  32680  pj3si  32688  pj3cor1i  32690  strlem3a  32733  strb  32739  hstrlem3a  32741  hstrbi  32747  spansncv2  32774  mdsl1i  32802  cvmdi  32805  mdexchi  32816  h1da  32830  mdsymlem6  32889  sumdmdii  32896  dmdbr5ati  32903  isoun  33174  xrge0tsmsd  33513  ordtrest2NEW  34433  pwsiga  34640  measiun  34729  dya2iocuni  34794  bnj518  35395  bnj1137  35504  bnj1136  35506  bnj1413  35544  bnj1417  35550  bnj60  35571  rankval4b  35607  r1filim  35612  trssfir1om  35621  fineqvnttrclselem3  35649  fineqvinfep  35651  tz9.1regs  35660  trssfir1omregs  35662  gblacfnacd  35699  onvf1odlem1  35700  onvf1odlem4  35703  vonf1oonfo  35712  erdszelem8  35777  cvmsss2  35853  cvmfolem  35858  fmlasucdisj  35978  satfun  35990  dfon2lem8  36367  dfon2lem9  36368  dfon2  36369  rdgprc  36371  nn0prpwlem  36941  ntruni  36946  clsint2  36948  fneint  36967  fnessref  36976  refssfne  36977  neibastop1  36978  neibastop2lem  36979  mh-inf3f1  37160  bj-0int  37851  bj-ismooredr  37859  relowlpssretop  38118  fvineqsneu  38165  fvineqsneq  38166  heicant  38404  mblfinlem1  38406  ftc2nc  38451  sdclem2  38492  fdc  38495  seqpo  38497  prdsbnd  38543  heibor  38571  rrnequiv  38585  0idl  38775  intidl  38779  unichnidl  38781  prnc  38817  refressn  39281  lsmcv2  39902  lcvexchlem4  39910  lcvexchlem5  39911  eqlkr  39972  paddclN  40715  pclfinN  40773  ldilcnv  40988  ldilco  40989  cdleme25dN  41229  cdlemj2  41695  tendocan  41697  erng1lem  41860  erngdvlem4-rN  41872  dihord2pre  42098  dihglblem2N  42167  dochvalr  42230  hdmap14lem12  42752  hdmap14lem13  42753  supinf  43109  fsuppind  43436  pellfundre  43722  pellfundge  43723  pellfundlb  43725  dford3lem1  43867  aomclem2  43896  oaabsb  44135  cantnf2  44166  ofoafg  44195  naddcnff  44203  naddwordnexlem3  44240  naddwordnexlem4  44242  pwinfi3  44403  iunrelexp0  44542  iunrelexpmin1  44548  iunrelexpmin2  44552  dftrcl3  44560  cnvtrclfv  44564  trclimalb2  44566  dfrtrcl3  44573  ntrneiel2  44926  ntrneik4w  44940  ntrrn  44962  gneispa  44970  gneispb  44971  addrcom  45297  iunconnlem2  45757  ssuzfz  46179  dvnprodlem3  46776  funressnfv  47931  cfsetsnfsetfo  47948  tz6.12-afv  48061  tz6.12-afv2  48128  otiunsndisjX  48167  uniimaprimaeqfv  48282  iccpartltu  48325  iccpartgtl  48326  iccpartleu  48328  iccpartgel  48329  fargshiftf  48340  fargshiftfva  48343  sbgoldbst  48694  bgoldbtbnd  48725  tgblthelfgott  48731  grimuhgr  48803  grimco  48805  isuspgrim0  48810  isuspgrimlem  48811  upgrimpths  48825  gricushgr  48833  grtriclwlk3  48861  stgr0  48876  uspgrlim  48908  grlicsym  48929  nnsgrp  49092  ellcoellss  49365  lindsrng01  49398  suppdm  49440  nn0sumshdiglem1  49551  setrec2fun  50618