Theorem ralrimiv 3132

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  ralrimiva  3133  ralrimivw  3137  ralrimdv  3139  reximdvaiOLD  3153  ralrimivv  3187  rr19.3v  3651  class2seteq  3694  rabssdv  4057  rzalALT  4492  disjord  5114  disjiund  5116  trin  5253  ralxfrALT  5397  otiunsndisj  5507  onmindif  6457  fnprb  7211  fntpb  7212  f1cdmsn  7285  ssorduni  7782  onminex  7805  onmindif2  7810  sucexeloniOLD  7813  suceloniOLD  7815  limuni3  7856  frxp  8134  poxp  8136  sexp2  8154  sexp3  8161  wfrlem15OLD  8346  onfununi  8364  onnseq  8367  tfrlem12  8412  tz7.48-2  8465  oaass  8582  omass  8601  oelim2  8616  oelimcl  8621  oaabs2  8670  omabs  8672  undifixp  8957  dom2lem  9015  isinf  9279  isinfOLD  9280  unblem4  9314  unbnn2  9316  marypha1lem  9456  supiso  9498  ordiso2  9538  card2inf  9578  elirrv  9619  wemapwe  9720  ttrclss  9743  trcl  9751  frr3g  9779  tz9.13  9814  rankval3b  9849  rankunb  9873  rankuni2b  9876  scott0  9909  updjud  9957  dfac8alem  10052  carduniima  10119  alephsmo  10125  alephval3  10133  iunfictbso  10137  dfac3  10144  dfac5lem5  10150  dfac12r  10170  dfac12k  10171  kmlem4  10177  kmlem11  10184  cfsuc  10280  cofsmo  10292  cfsmolem  10293  coftr  10296  alephsing  10299  infpssrlem3  10328  fin23lem30  10365  isf32lem2  10377  isf32lem3  10378  isf34lem6  10403  fin1a2lem11  10433  fin1a2lem13  10435  fin1a2s  10437  axcc2lem  10459  domtriomlem  10465  axdc3lem2  10474  axdc4lem  10478  axcclem  10480  axdclem2  10543  iundom2g  10563  uniimadom  10567  cardmin  10587  alephval2  10595  alephreg  10605  fpwwe2lem11  10664  wunex2  10761  wuncval2  10770  tskwe2  10796  inar1  10798  tskuni  10806  gruun  10829  intgru  10837  grutsk1  10844  genpcl  11031  ltexprlem5  11063  suplem1pr  11075  supexpr  11077  supsrlem  11134  axpre-sup  11192  negfi  12200  supaddc  12218  supadd  12219  supmul1  12220  supmullem1  12221  supmul  12223  peano5nni  12252  uzind  12694  zindd  12703  uzwo  12936  lbzbi  12961  xrsupsslem  13332  xrinfmsslem  13333  supxrun  13341  supxrpnf  13343  supxrunb1  13344  supxrunb2  13345  icoshftf1o  13497  flval3  13838  axdc4uzlem  14007  tpfo  14522  wrdnfi  14569  ccatrn  14610  ccatalpha  14614  2cshw  14834  cshweqrep  14842  s3iunsndisj  14990  rtrclreclem4  15083  dfrtrcl2  15084  01sqrexlem1  15264  01sqrexlem6  15269  fsum0diag2  15802  alzdvds  16340  gcdcllem1  16519  lcmfunsnlem2lem1  16658  lcmfunsnlem2lem2  16659  maxprmfct  16729  hashgcdeq  16810  unbenlem  16929  vdwlem6  17007  vdwlem10  17011  firest  17453  mrieqv2d  17658  iscatd  17692  initoeu2  18037  setcmon  18108  setcepi  18109  fullestrcsetc  18171  fullsetcestrc  18186  isglbd  18528  isacs4lem  18563  acsfiindd  18572  acsmapd  18573  psss  18599  sgrpidmnd  18726  pwmnd  18924  ghmrn  19221  ghmpreima  19230  cntz2ss  19327  symgextres  19416  psgnunilem2  19486  lsmsubg  19645  efgsfo  19730  gsumzaddlem  19912  gsummptnn0fzfv  19978  dmdprdd  19992  dprd2da  20035  ablsimpgprmd  20108  imasring  20300  01eq0ring  20503  isabvd  20786  issrngd  20829  islssd  20906  lbsextlem3  21135  lbsextlem4  21136  lidldvgen  21311  pzriprnglem4  21462  pzriprnglem7  21465  pzriprnglem13  21471  psgnghm  21565  isphld  21639  frlmsslsp  21783  mp2pm2mplem4  22782  tgcl  22942  distop  22968  indistopon  22974  pptbas  22981  toponmre  23066  opnnei  23093  neiuni  23095  neindisj2  23096  ordtrest2  23177  cnpnei  23237  cnindis  23265  cmpcld  23375  uncmp  23376  hauscmplem  23379  2ndc1stc  23424  1stcrest  23426  1stcelcls  23434  llyrest  23458  nllyrest  23459  cldllycmp  23468  reftr  23487  locfincf  23504  comppfsc  23505  txcls  23577  ptpjcn  23584  ptclsg  23588  dfac14lem  23590  xkoccn  23592  txlly  23609  txnlly  23610  ptrescn  23612  tx1stc  23623  xkoco1cn  23630  xkoco2cn  23631  xkococn  23633  xkoinjcn  23660  qtopeu  23689  hmeofval  23731  ordthmeolem  23774  isfild  23831  fbasrn  23857  trfil2  23860  flimclslem  23957  fclsrest  23997  fclscf  23998  flimfcls  23999  alexsubALTlem1  24020  alexsubALTlem2  24021  alexsubALTlem3  24022  alexsubALT  24024  qustgpopn  24093  isxmetd  24300  imasdsf1olem  24347  blcls  24482  prdsxmslem2  24505  metustfbas  24533  dscmet  24548  nrmmetd  24550  reperflem  24795  reconnlem2  24804  xrge0tsms  24811  fsumcn  24849  cnheibor  24942  tcphcph  25226  lmmbr  25247  caubl  25297  ivthlem1  25441  ovolctb  25480  ovoliunlem2  25493  ovolscalem1  25503  ovolicc2  25512  voliunlem3  25542  ismbfd  25629  mbfimaopnlem  25645  itg2le  25729  ellimc2  25867  c1liplem1  25990  plyeq0lem  26204  dgreq0  26260  aannenlem1  26325  pilem2  26451  cxpcn3lem  26745  scvxcvx  26984  musum  27189  fsumdvdsmul  27193  dchrisum0flb  27509  ostth2lem2  27633  sltval2  27656  nolesgn2ores  27672  nogesgn1ores  27674  nosupres  27707  nosupbnd2lem1  27715  noinfres  27722  noinfbnd2lem1  27730  scutun12  27810  madebdayim  27881  precsexlem9  28194  noseqind  28253  zs12bday  28379  numedglnl  29108  upgrreslem  29268  umgrreslem  29269  nbuhgr  29307  nbumgr  29311  uhgrnbgr0nb  29318  nbusgrf1o0  29333  uvtxnbgrvtx  29357  cusgrfilem2  29421  uspgr2wlkeq  29611  wwlks  29802  iswwlksnon  29820  rusgr0edg  29940  clwwlkccatlem  29955  clwwisshclwwslem  29980  clwwlkn  29992  clwwlknon  30056  3cyclfrgrrn  30252  vdgn1frgrv3  30263  2wspmdisj  30303  numclwlk2lem2f1o  30345  frgrregord013  30361  htthlem  30883  ocsh  31249  shintcli  31295  pjss2coi  32130  pjnormssi  32134  pjclem4  32165  pj3si  32173  pj3cor1i  32175  strlem3a  32218  strb  32224  hstrlem3a  32226  hstrbi  32232  spansncv2  32259  mdsl1i  32287  cvmdi  32290  mdexchi  32301  h1da  32315  mdsymlem6  32374  sumdmdii  32381  dmdbr5ati  32388  isoun  32658  supssd  32668  infssd  32669  xrge0tsmsd  33011  ordtrest2NEW  33863  pwsiga  34072  measiun  34160  dya2iocuni  34226  bnj518  34841  bnj1137  34950  bnj1136  34952  bnj1413  34990  bnj1417  34996  bnj60  35017  gblacfnacd  35054  subgrwlk  35078  erdszelem8  35144  cvmsss2  35220  cvmfolem  35225  fmlasucdisj  35345  satfun  35357  dfon2lem8  35732  dfon2lem9  35733  dfon2  35734  rdgprc  35736  nn0prpwlem  36264  ntruni  36269  clsint2  36271  fneint  36290  fnessref  36299  refssfne  36300  neibastop1  36301  neibastop2lem  36302  bj-0int  37043  bj-ismooredr  37051  relowlpssretop  37306  fvineqsneu  37353  fvineqsneq  37354  heicant  37603  mblfinlem1  37605  ftc2nc  37650  sdclem2  37690  fdc  37693  seqpo  37695  prdsbnd  37741  heibor  37769  rrnequiv  37783  0idl  37973  intidl  37977  unichnidl  37979  prnc  38015  uniqsALTV  38271  refressn  38385  lsmcv2  38971  lcvexchlem4  38979  lcvexchlem5  38980  eqlkr  39041  paddclN  39785  pclfinN  39843  ldilcnv  40058  ldilco  40059  cdleme25dN  40299  cdlemj2  40765  tendocan  40767  erng1lem  40930  erngdvlem4-rN  40942  dihord2pre  41168  dihglblem2N  41237  dochvalr  41300  hdmap14lem12  41822  hdmap14lem13  41823  supinf  42223  fsuppind  42545  pellfundre  42837  pellfundge  42838  pellfundlb  42840  dford3lem1  42983  aomclem2  43012  oaabsb  43252  cantnf2  43283  ofoafg  43312  naddcnff  43320  naddwordnexlem3  43357  naddwordnexlem4  43359  pwinfi3  43521  iunrelexp0  43660  iunrelexpmin1  43666  iunrelexpmin2  43670  dftrcl3  43678  cnvtrclfv  43682  trclimalb2  43684  dfrtrcl3  43691  ntrneiel2  44044  ntrneik4w  44058  ntrrn  44080  gneispa  44088  gneispb  44089  addrcom  44439  iunconnlem2  44900  ssuzfz  45305  dvnprodlem3  45908  funressnfv  47001  cfsetsnfsetfo  47018  tz6.12-afv  47131  tz6.12-afv2  47198  otiunsndisjX  47237  uniimaprimaeqfv  47315  iccpartltu  47358  iccpartgtl  47359  iccpartleu  47361  iccpartgel  47362  fargshiftf  47373  fargshiftfva  47376  sbgoldbst  47711  bgoldbtbnd  47742  tgblthelfgott  47748  isuspgrim0  47818  isuspgrimlem  47820  grimuhgr  47824  grimco  47826  gricushgr  47832  grtriclwlk3  47858  stgr0  47873  uspgrlim  47905  grlicsym  47919  nnsgrp  48039  ellcoellss  48298  lindsrng01  48331  suppdm  48373  nn0sumshdiglem1  48488  setrec2fun  49207