Theorem ralrimiv 3162

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

Syntax hints:   → wi 4   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  ralrimiva  3163  ralrimivw  3167  ralrimdv  3169  ralrimivv  3212  rr19.3v  3633  class2seteq  3674  rabssdv  4034  rzalALT  4459  r19.3rzv  4467  disjord  5100  disjiund  5102  trun  5231  trin  5232  ralxfrALT  5387  otiunsndisj  5504  onmindif  6456  fnprb  7207  fntpb  7208  f1cdmsn  7281  ssorduni  7778  onminex  7801  onmindif2  7806  limuni3  7848  frxp  8122  poxp  8124  sexp2  8142  sexp3  8149  onfununi  8328  onnseq  8331  tfrlem12  8376  tz7.48-2  8429  oaass  8546  omass  8565  oelim2  8581  oelimcl  8586  oaabs2  8635  omabs  8637  uniqs  8771  undifixp  8932  dom2lem  8989  isinf  9225  unblem4  9255  unbnn2  9257  marypha1lem  9393  supssd  9423  supiso  9436  infssd  9454  ordiso2  9477  card2inf  9517  elirrvOLDOLD  9561  wemapwe  9666  ttrclss  9689  trcl  9697  frr3g  9728  tz9.13  9763  rankval3b  9798  rankunb  9822  rankuni2b  9825  scott0  9860  updjud  9920  dfac8alem  10013  carduniima  10080  alephsmo  10086  alephval3  10094  iunfictbso  10098  dfac3  10105  dfac5lem5  10111  dfac12r  10130  dfac12k  10131  kmlem4  10137  kmlem11  10144  cfsuc  10241  cofsmo  10253  cfsmolem  10254  coftr  10257  alephsing  10260  infpssrlem3  10289  fin23lem30  10326  isf32lem2  10338  isf32lem3  10339  isf34lem6  10364  fin1a2lem11  10394  fin1a2lem13  10396  fin1a2s  10398  axcc2lem  10420  domtriomlem  10426  axdc3lem2  10435  axdc4lem  10439  axcclem  10441  axdclem2  10504  iundom2g  10524  uniimadom  10528  cardmin  10548  alephval2  10557  alephreg  10567  fpwwe2lem11  10626  wunex2  10723  wuncval2  10732  tskwe2  10758  inar1  10760  tskuni  10768  gruun  10791  intgru  10799  grutsk1  10806  genpcl  10993  ltexprlem5  11025  suplem1pr  11037  supexpr  11039  supsrlem  11096  axpre-sup  11154  negfi  12164  supaddc  12182  supadd  12183  supmul1  12184  supmullem1  12185  supmul  12187  peano5nni  12236  uzind  12688  zindd  12697  uzwo  12935  lbzbi  12960  xrsupsslem  13333  xrinfmsslem  13334  supxrun  13342  supxrpnf  13344  supxrunb1  13345  supxrunb2  13346  icoshftf1o  13501  flval3  13848  axdc4uzlem  14019  tpfo  14537  wrdnfi  14585  ccatrn  14627  ccatalpha  14631  2cshw  14850  cshweqrep  14858  s3iunsndisj  15005  rtrclreclem4  15098  dfrtrcl2  15099  01sqrexlem1  15293  01sqrexlem6  15298  fsum0diag2  15834  alzdvds  16378  gcdcllem1  16557  lcmfunsnlem2lem1  16696  lcmfunsnlem2lem2  16697  maxprmfct  16768  hashgcdeq  16849  unbenlem  16968  vdwlem6  17046  vdwlem10  17050  firest  17485  mrieqv2d  17695  iscatd  17729  initoeu2  18073  setcmon  18144  setcepi  18145  fullestrcsetc  18207  fullsetcestrc  18222  isglbd  18565  isacs4lem  18600  acsfiindd  18609  acsmapd  18610  psss  18636  sgrpidmnd  18797  pwmnd  18999  ghmrn  19299  ghmpreima  19308  cntz2ss  19405  symgextres  19495  psgnunilem2  19565  lsmsubg  19724  efgsfo  19809  gsumzaddlem  19991  gsummptnn0fzfv  20057  dmdprdd  20071  dprd2da  20114  ablsimpgprmd  20187  imasring  20412  01eq0ring  20614  isabvd  20893  issrngd  20936  islssd  21034  lbsextlem3  21262  lbsextlem4  21263  unichnlidl  21340  lidldvgen  21471  pzriprnglem4  21603  pzriprnglem7  21606  pzriprnglem13  21612  psgnghm  21699  isphld  21773  frlmsslsp  21915  mp2pm2mplem4  22935  tgcl  23095  distop  23121  indistopon  23127  pptbas  23134  toponmre  23219  opnnei  23246  neiuni  23248  neindisj2  23249  ordtrest2  23330  cnpnei  23390  cnindis  23418  cmpcld  23528  uncmp  23529  hauscmplem  23532  2ndc1stc  23577  1stcrest  23579  1stcelcls  23587  llyrest  23611  nllyrest  23612  cldllycmp  23621  reftr  23640  locfincf  23657  comppfsc  23658  txcls  23730  ptpjcn  23737  ptclsg  23741  dfac14lem  23743  xkoccn  23745  txlly  23762  txnlly  23763  ptrescn  23765  tx1stc  23776  xkoco1cn  23783  xkoco2cn  23784  xkococn  23786  xkoinjcn  23813  qtopeu  23842  hmeofval  23884  ordthmeolem  23927  isfild  23984  fbasrn  24010  trfil2  24013  flimclslem  24110  fclsrest  24150  fclscf  24151  flimfcls  24152  alexsubALTlem1  24173  alexsubALTlem2  24174  alexsubALTlem3  24175  alexsubALT  24177  qustgpopn  24246  isxmetd  24452  imasdsf1olem  24499  blcls  24632  prdsxmslem2  24655  metustfbas  24683  dscmet  24698  nrmmetd  24700  reperflem  24945  reconnlem2  24954  xrge0tsms  24961  fsumcn  24998  cnheibor  25083  tcphcph  25365  lmmbr  25386  caubl  25436  ivthlem1  25579  ovolctb  25618  ovoliunlem2  25631  ovolscalem1  25641  ovolicc2  25650  voliunlem3  25680  ismbfd  25767  mbfimaopnlem  25783  itg2le  25867  ellimc2  26005  c1liplem1  26124  plyeq0lem  26336  dgreq0  26391  aannenlem1  26458  pilem2  26581  cxpcn3lem  26878  scvxcvx  27116  musum  27321  fsumdvdsmul  27325  dchrisum0flb  27640  ostth2lem2  27764  ltsval2  27786  nolesgn2ores  27802  nogesgn1ores  27804  nosupres  27837  nosupbnd2lem1  27845  noinfres  27852  noinfbnd2lem1  27860  cutsun12  27949  madebdayim  28047  precsexlem9  28374  addonbday  28438  noseqind  28451  z12zsodd  28641  numedglnl  29435  upgrreslem  29595  umgrreslem  29596  nbuhgr  29634  nbumgr  29638  uhgrnbgr0nb  29645  nbusgrf1o0  29660  uvtxnbgrvtx  29684  cusgrfilem2  29747  uspgr2wlkeq  29936  wwlks  30125  iswwlksnon  30143  rusgr0edg  30266  clwwlkccatlem  30281  clwwisshclwwslem  30306  clwwlkn  30318  clwwlknon  30382  3cyclfrgrrn  30578  vdgn1frgrv3  30589  2wspmdisj  30629  numclwlk2lem2f1o  30671  frgrregord013  30687  htthlem  31210  ocsh  31576  shintcli  31622  pjss2coi  32457  pjnormssi  32461  pjclem4  32492  pj3si  32500  pj3cor1i  32502  strlem3a  32545  strb  32551  hstrlem3a  32553  hstrbi  32559  spansncv2  32586  mdsl1i  32614  cvmdi  32617  mdexchi  32628  h1da  32642  mdsymlem6  32701  sumdmdii  32708  dmdbr5ati  32715  isoun  32988  xrge0tsmsd  33334  ordtrest2NEW  34258  pwsiga  34465  measiun  34553  dya2iocuni  34618  bnj518  35219  bnj1137  35328  bnj1136  35330  bnj1413  35368  bnj1417  35374  bnj60  35395  rankval4b  35436  r1filim  35441  trssfir1om  35448  fineqvnttrclselem3  35469  fineqvinfep  35471  tz9.1regs  35480  trssfir1omregs  35482  gblacfnacd  35519  onvf1odlem1  35520  onvf1odlem4  35523  vonf1oonfo  35532  subgrwlk  35557  erdszelem8  35623  cvmsss2  35699  cvmfolem  35704  fmlasucdisj  35824  satfun  35836  dfon2lem8  36213  dfon2lem9  36214  dfon2  36215  rdgprc  36217  nn0prpwlem  36756  ntruni  36761  clsint2  36763  fneint  36782  fnessref  36791  refssfne  36792  neibastop1  36793  neibastop2lem  36794  mh-inf3f1  36975  bj-0int  37666  bj-ismooredr  37674  relowlpssretop  37933  fvineqsneu  37980  fvineqsneq  37981  heicant  38229  mblfinlem1  38231  ftc2nc  38276  sdclem2  38316  fdc  38319  seqpo  38321  prdsbnd  38367  heibor  38395  rrnequiv  38409  0idl  38599  intidl  38603  unichnidl  38605  prnc  38641  refressn  39107  lsmcv2  39728  lcvexchlem4  39736  lcvexchlem5  39737  eqlkr  39798  paddclN  40541  pclfinN  40599  ldilcnv  40814  ldilco  40815  cdleme25dN  41055  cdlemj2  41521  tendocan  41523  erng1lem  41686  erngdvlem4-rN  41698  dihord2pre  41924  dihglblem2N  41993  dochvalr  42056  hdmap14lem12  42578  hdmap14lem13  42579  supinf  42935  fsuppind  43249  pellfundre  43535  pellfundge  43536  pellfundlb  43538  dford3lem1  43680  aomclem2  43709  oaabsb  43948  cantnf2  43979  ofoafg  44008  naddcnff  44016  naddwordnexlem3  44053  naddwordnexlem4  44055  pwinfi3  44216  iunrelexp0  44355  iunrelexpmin1  44361  iunrelexpmin2  44365  dftrcl3  44373  cnvtrclfv  44377  trclimalb2  44379  dfrtrcl3  44386  ntrneiel2  44739  ntrneik4w  44753  ntrrn  44775  gneispa  44783  gneispb  44784  addrcom  45110  iunconnlem2  45570  ssuzfz  45992  dvnprodlem3  46589  funressnfv  47704  cfsetsnfsetfo  47721  tz6.12-afv  47834  tz6.12-afv2  47901  otiunsndisjX  47940  uniimaprimaeqfv  48055  iccpartltu  48098  iccpartgtl  48099  iccpartleu  48101  iccpartgel  48102  fargshiftf  48113  fargshiftfva  48116  sbgoldbst  48467  bgoldbtbnd  48498  tgblthelfgott  48504  grimuhgr  48576  grimco  48578  isuspgrim0  48583  isuspgrimlem  48584  upgrimpths  48598  gricushgr  48606  grtriclwlk3  48634  stgr0  48649  uspgrlim  48681  grlicsym  48702  nnsgrp  48866  ellcoellss  49135  lindsrng01  49168  suppdm  49210  nn0sumshdiglem1  49321  setrec2fun  50390