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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

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

This theorem is used by:  ralrimiva  3156  ralrimivw  3160  ralrimdv  3162  ralrimivv  3205  rr19.3v  3625  class2seteq  3666  rabssdv  4027  rzalALT  4455  r19.3rzv  4463  disjord  5097  disjiund  5099  trun  5228  trin  5229  ralxfrALT  5385  otiunsndisj  5502  onmindif  6455  fnprb  7206  fntpb  7207  f1cdmsn  7280  ssorduni  7776  onminex  7799  onmindif2  7804  limuni3  7846  frxp  8120  poxp  8122  sexp2  8140  sexp3  8147  onfununi  8326  onnseq  8329  tfrlem12  8374  tz7.48-2  8427  oaass  8544  omass  8563  oelim2  8579  oelimcl  8584  oaabs2  8633  omabs  8635  uniqs  8769  undifixp  8930  dom2lem  8987  isinf  9223  unblem4  9253  unbnn2  9255  marypha1lem  9391  supssd  9421  supiso  9434  infssd  9452  ordiso2  9475  card2inf  9515  elirrvOLDOLD  9559  wemapwe  9664  ttrclss  9687  trcl  9695  frr3g  9726  tz9.13  9761  rankval3b  9796  rankunb  9820  rankuni2b  9823  scott0b  9864  scott0OLD  9865  updjud  9927  dfac8alem  10020  carduniima  10087  alephsmo  10093  alephval3  10101  iunfictbso  10105  dfac3  10112  dfac5lem5  10118  dfac12r  10137  dfac12k  10138  kmlem4  10144  kmlem11  10151  cfsuc  10247  cofsmo  10259  cfsmolem  10260  coftr  10263  alephsing  10266  infpssrlem3  10295  fin23lem30  10332  isf32lem2  10344  isf32lem3  10345  isf34lem6  10370  fin1a2lem11  10400  fin1a2lem13  10402  fin1a2s  10404  axcc2lem  10426  domtriomlem  10432  axdc3lem2  10441  axdc4lem  10445  axcclem  10447  axdclem2  10510  iundom2g  10530  uniimadom  10534  cardmin  10554  alephval2  10563  alephreg  10573  fpwwe2lem11  10632  wunex2  10729  wuncval2  10738  tskwe2  10764  inar1  10766  tskuni  10774  gruun  10797  intgru  10805  grutsk1  10812  genpcl  10999  ltexprlem5  11031  suplem1pr  11043  supexpr  11045  supsrlem  11102  axpre-sup  11160  negfi  12170  supaddc  12188  supadd  12189  supmul1  12190  supmullem1  12191  supmul  12193  peano5nni  12242  uzind  12694  zindd  12703  uzwo  12941  lbzbi  12966  xrsupsslem  13339  xrinfmsslem  13340  supxrun  13348  supxrpnf  13350  supxrunb1  13351  supxrunb2  13352  icoshftf1o  13507  flval3  13855  axdc4uzlem  14026  tpfo  14544  wrdnfi  14592  ccatrn  14634  ccatalpha  14638  2cshw  14857  cshweqrep  14865  s3iunsndisj  15012  rtrclreclem4  15105  dfrtrcl2  15106  01sqrexlem1  15300  01sqrexlem6  15305  fsum0diag2  15841  alzdvds  16384  gcdcllem1  16563  lcmfunsnlem2lem1  16702  lcmfunsnlem2lem2  16703  maxprmfct  16774  hashgcdeq  16855  unbenlem  16974  vdwlem6  17052  vdwlem10  17056  firest  17491  mrieqv2d  17701  iscatd  17735  initoeu2  18079  setcmon  18150  setcepi  18151  fullestrcsetc  18213  fullsetcestrc  18228  isglbd  18571  isacs4lem  18606  acsfiindd  18615  acsmapd  18616  psss  18642  sgrpidmnd  18803  pwmnd  19005  ghmrn  19305  ghmpreima  19314  cntz2ss  19411  symgextres  19501  psgnunilem2  19571  lsmsubg  19730  efgsfo  19815  gsumzaddlem  19997  gsummptnn0fzfv  20063  dmdprdd  20077  dprd2da  20120  ablsimpgprmd  20193  imasring  20419  01eq0ring  20639  isabvd  20926  issrngd  20969  islssd  21067  lbsextlem3  21295  lbsextlem4  21296  unichnlidl  21373  lidldvgen  21513  pzriprnglem4  21645  pzriprnglem7  21648  pzriprnglem13  21654  psgnghm  21741  isphld  21815  frlmsslsp  21957  mp2pm2mplem4  22977  tgcl  23137  distop  23163  indistopon  23169  pptbas  23176  toponmre  23261  opnnei  23288  neiuni  23290  neindisj2  23291  ordtrest2  23372  cnpnei  23432  cnindis  23460  cmpcld  23570  uncmp  23571  hauscmplem  23574  2ndc1stc  23619  1stcrest  23621  1stcelcls  23629  llyrest  23653  nllyrest  23654  cldllycmp  23663  reftr  23682  locfincf  23699  comppfsc  23700  txcls  23772  ptpjcn  23779  ptclsg  23783  dfac14lem  23785  xkoccn  23787  txlly  23804  txnlly  23805  ptrescn  23807  tx1stc  23818  xkoco1cn  23825  xkoco2cn  23826  xkococn  23828  xkoinjcn  23855  qtopeu  23884  hmeofval  23926  ordthmeolem  23969  isfild  24026  fbasrn  24052  trfil2  24055  flimclslem  24152  fclsrest  24192  fclscf  24193  flimfcls  24194  alexsubALTlem1  24215  alexsubALTlem2  24216  alexsubALTlem3  24217  alexsubALT  24219  qustgpopn  24288  isxmetd  24494  imasdsf1olem  24541  blcls  24674  prdsxmslem2  24697  metustfbas  24725  dscmet  24740  nrmmetd  24742  reperflem  24987  reconnlem2  24996  xrge0tsms  25003  fsumcn  25040  cnheibor  25125  tcphcph  25407  lmmbr  25428  caubl  25478  ivthlem1  25621  ovolctb  25660  ovoliunlem2  25673  ovolscalem1  25683  ovolicc2  25692  voliunlem3  25722  ismbfd  25809  mbfimaopnlem  25825  itg2le  25909  ellimc2  26047  c1liplem1  26166  plyeq0lem  26378  dgreq0  26433  aannenlem1  26502  pilem2  26626  cxpcn3lem  26923  scvxcvx  27161  musum  27366  fsumdvdsmul  27370  dchrisum0flb  27685  ostth2lem2  27809  ltsval2  27831  nolesgn2ores  27847  nogesgn1ores  27849  nosupres  27882  nosupbnd2lem1  27890  noinfres  27897  noinfbnd2lem1  27905  cutsun12  27994  madebdayim  28092  precsexlem9  28419  addonbday  28483  noseqind  28496  z12zsodd  28686  numedglnl  29505  upgrreslem  29665  umgrreslem  29666  nbuhgr  29704  nbumgr  29708  uhgrnbgr0nb  29715  nbusgrf1o0  29730  uvtxnbgrvtx  29754  cusgrfilem2  29817  uspgr2wlkeq  30006  wwlks  30195  iswwlksnon  30213  rusgr0edg  30336  clwwlkccatlem  30351  clwwisshclwwslem  30376  clwwlkn  30388  clwwlknon  30452  3cyclfrgrrn  30648  vdgn1frgrv3  30659  2wspmdisj  30699  numclwlk2lem2f1o  30741  frgrregord013  30757  htthlem  31280  ocsh  31646  shintcli  31692  pjss2coi  32527  pjnormssi  32531  pjclem4  32562  pj3si  32570  pj3cor1i  32572  strlem3a  32615  strb  32621  hstrlem3a  32623  hstrbi  32629  spansncv2  32656  mdsl1i  32684  cvmdi  32687  mdexchi  32698  h1da  32712  mdsymlem6  32771  sumdmdii  32778  dmdbr5ati  32785  isoun  33058  xrge0tsmsd  33402  ordtrest2NEW  34322  pwsiga  34529  measiun  34617  dya2iocuni  34682  bnj518  35283  bnj1137  35392  bnj1136  35394  bnj1413  35432  bnj1417  35438  bnj60  35459  rankval4b  35502  r1filim  35507  trssfir1om  35516  fineqvnttrclselem3  35544  fineqvinfep  35546  tz9.1regs  35555  trssfir1omregs  35557  gblacfnacd  35594  onvf1odlem1  35595  onvf1odlem4  35598  vonf1oonfo  35607  subgrwlk  35632  erdszelem8  35698  cvmsss2  35774  cvmfolem  35779  fmlasucdisj  35899  satfun  35911  dfon2lem8  36288  dfon2lem9  36289  dfon2  36290  rdgprc  36292  nn0prpwlem  36861  ntruni  36866  clsint2  36868  fneint  36887  fnessref  36896  refssfne  36897  neibastop1  36898  neibastop2lem  36899  mh-inf3f1  37080  bj-0int  37771  bj-ismooredr  37779  relowlpssretop  38038  fvineqsneu  38085  fvineqsneq  38086  heicant  38334  mblfinlem1  38336  ftc2nc  38381  sdclem2  38421  fdc  38424  seqpo  38426  prdsbnd  38472  heibor  38500  rrnequiv  38514  0idl  38704  intidl  38708  unichnidl  38710  prnc  38746  refressn  39210  lsmcv2  39831  lcvexchlem4  39839  lcvexchlem5  39840  eqlkr  39901  paddclN  40644  pclfinN  40702  ldilcnv  40917  ldilco  40918  cdleme25dN  41158  cdlemj2  41624  tendocan  41626  erng1lem  41789  erngdvlem4-rN  41801  dihord2pre  42027  dihglblem2N  42096  dochvalr  42159  hdmap14lem12  42681  hdmap14lem13  42682  supinf  43038  fsuppind  43350  pellfundre  43636  pellfundge  43637  pellfundlb  43639  dford3lem1  43781  aomclem2  43810  oaabsb  44049  cantnf2  44080  ofoafg  44109  naddcnff  44117  naddwordnexlem3  44154  naddwordnexlem4  44156  pwinfi3  44317  iunrelexp0  44456  iunrelexpmin1  44462  iunrelexpmin2  44466  dftrcl3  44474  cnvtrclfv  44478  trclimalb2  44480  dfrtrcl3  44487  ntrneiel2  44840  ntrneik4w  44854  ntrrn  44876  gneispa  44884  gneispb  44885  addrcom  45211  iunconnlem2  45671  ssuzfz  46093  dvnprodlem3  46690  funressnfv  47808  cfsetsnfsetfo  47825  tz6.12-afv  47938  tz6.12-afv2  48005  otiunsndisjX  48044  uniimaprimaeqfv  48159  iccpartltu  48202  iccpartgtl  48203  iccpartleu  48205  iccpartgel  48206  fargshiftf  48217  fargshiftfva  48220  sbgoldbst  48571  bgoldbtbnd  48602  tgblthelfgott  48608  grimuhgr  48680  grimco  48682  isuspgrim0  48687  isuspgrimlem  48688  upgrimpths  48702  gricushgr  48710  grtriclwlk3  48738  stgr0  48753  uspgrlim  48785  grlicsym  48806  nnsgrp  48970  ellcoellss  49243  lindsrng01  49276  suppdm  49318  nn0sumshdiglem1  49429  setrec2fun  50498