Theorem ralrimiv 3146

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  ralrimiva  3147  ralrimivw  3151  ralrimdv  3153  reximdvaiOLD  3167  ralrimivv  3199  raleleqOLD  3341  rr19.3v  3658  class2seteq  3701  rabssdv  4073  rzalALT  4510  disjord  5137  disjiund  5139  trin  5278  ralxfrALT  5414  otiunsndisj  5521  onmindif  6457  fnprb  7210  fntpb  7211  f1cdmsn  7280  ssorduni  7766  onminex  7790  onmindif2  7795  sucexeloniOLD  7798  suceloniOLD  7800  limuni3  7841  frxp  8112  poxp  8114  sexp2  8132  sexp3  8139  wfrlem15OLD  8323  onfununi  8341  onnseq  8344  tfrlem12  8389  tz7.48-2  8442  oaass  8561  omass  8580  oelim2  8595  oelimcl  8600  oaabs2  8648  omabs  8650  undifixp  8928  dom2lem  8988  isinf  9260  isinfOLD  9261  unblem4  9298  unbnn2  9300  marypha1lem  9428  supiso  9470  ordiso2  9510  card2inf  9550  elirrv  9591  wemapwe  9692  ttrclss  9715  trcl  9723  frr3g  9751  tz9.13  9786  rankval3b  9821  rankunb  9845  rankuni2b  9848  scott0  9881  updjud  9929  dfac8alem  10024  carduniima  10091  alephsmo  10097  alephval3  10105  iunfictbso  10109  dfac3  10116  dfac5lem5  10122  dfac12r  10141  dfac12k  10142  kmlem4  10148  kmlem11  10155  cfsuc  10252  cofsmo  10264  cfsmolem  10265  coftr  10268  alephsing  10271  infpssrlem3  10300  fin23lem30  10337  isf32lem2  10349  isf32lem3  10350  isf34lem6  10375  fin1a2lem11  10405  fin1a2lem13  10407  fin1a2s  10409  axcc2lem  10431  domtriomlem  10437  axdc3lem2  10446  axdc4lem  10450  axcclem  10452  axdclem2  10515  iundom2g  10535  uniimadom  10539  cardmin  10559  alephval2  10567  alephreg  10577  fpwwe2lem11  10636  wunex2  10733  wuncval2  10742  tskwe2  10768  inar1  10770  tskuni  10778  gruun  10801  intgru  10809  grutsk1  10816  genpcl  11003  ltexprlem5  11035  suplem1pr  11047  supexpr  11049  supsrlem  11106  axpre-sup  11164  negfi  12163  supaddc  12181  supadd  12182  supmul1  12183  supmullem1  12184  supmul  12186  peano5nni  12215  uzind  12654  zindd  12663  uzwo  12895  lbzbi  12920  xrsupsslem  13286  xrinfmsslem  13287  supxrun  13295  supxrpnf  13297  supxrunb1  13298  supxrunb2  13299  icoshftf1o  13451  flval3  13780  axdc4uzlem  13948  wrdnfi  14498  ccatrn  14539  ccatalpha  14543  2cshw  14763  cshweqrep  14771  s3iunsndisj  14915  rtrclreclem4  15008  dfrtrcl2  15009  01sqrexlem1  15189  01sqrexlem6  15194  fsum0diag2  15729  alzdvds  16263  gcdcllem1  16440  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  maxprmfct  16646  hashgcdeq  16722  unbenlem  16841  vdwlem6  16919  vdwlem10  16923  firest  17378  mrieqv2d  17583  iscatd  17617  initoeu2  17966  setcmon  18037  setcepi  18038  fullestrcsetc  18103  fullsetcestrc  18118  isglbd  18462  isacs4lem  18497  acsfiindd  18506  acsmapd  18507  psss  18533  sgrpidmnd  18630  pwmnd  18818  ghmrn  19105  ghmpreima  19114  cntz2ss  19199  symgextres  19293  psgnunilem2  19363  lsmsubg  19522  efgsfo  19607  gsumzaddlem  19789  gsummptnn0fzfv  19855  dmdprdd  19869  dprd2da  19912  ablsimpgprmd  19985  imasring  20143  01eq0ring  20305  isabvd  20428  issrngd  20469  islssd  20546  lbsextlem3  20773  lbsextlem4  20774  lidldvgen  20893  psgnghm  21133  isphld  21207  frlmsslsp  21351  mp2pm2mplem4  22311  tgcl  22472  distop  22498  indistopon  22504  pptbas  22511  toponmre  22597  opnnei  22624  neiuni  22626  neindisj2  22627  ordtrest2  22708  cnpnei  22768  cnindis  22796  cmpcld  22906  uncmp  22907  hauscmplem  22910  2ndc1stc  22955  1stcrest  22957  1stcelcls  22965  llyrest  22989  nllyrest  22990  cldllycmp  22999  reftr  23018  locfincf  23035  comppfsc  23036  txcls  23108  ptpjcn  23115  ptclsg  23119  dfac14lem  23121  xkoccn  23123  txlly  23140  txnlly  23141  ptrescn  23143  tx1stc  23154  xkoco1cn  23161  xkoco2cn  23162  xkococn  23164  xkoinjcn  23191  qtopeu  23220  hmeofval  23262  ordthmeolem  23305  isfild  23362  fbasrn  23388  trfil2  23391  flimclslem  23488  fclsrest  23528  fclscf  23529  flimfcls  23530  alexsubALTlem1  23551  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALT  23555  qustgpopn  23624  isxmetd  23832  imasdsf1olem  23879  blcls  24015  prdsxmslem2  24038  metustfbas  24066  dscmet  24081  nrmmetd  24083  reperflem  24334  reconnlem2  24343  xrge0tsms  24350  fsumcn  24386  cnheibor  24471  tcphcph  24754  lmmbr  24775  caubl  24825  ivthlem1  24968  ovolctb  25007  ovoliunlem2  25020  ovolscalem1  25030  ovolicc2  25039  voliunlem3  25069  ismbfd  25156  mbfimaopnlem  25172  itg2le  25257  ellimc2  25394  c1liplem1  25513  plyeq0lem  25724  dgreq0  25779  aannenlem1  25841  pilem2  25964  cxpcn3lem  26255  scvxcvx  26490  musum  26695  dchrisum0flb  27013  ostth2lem2  27137  sltval2  27159  nolesgn2ores  27175  nogesgn1ores  27177  nosupres  27210  nosupbnd2lem1  27218  noinfres  27225  noinfbnd2lem1  27233  scutun12  27311  madebdayim  27382  precsexlem9  27661  numedglnl  28404  upgrreslem  28561  umgrreslem  28562  nbuhgr  28600  nbumgr  28604  uhgrnbgr0nb  28611  nbusgrf1o0  28626  uvtxnbgrvtx  28650  cusgrfilem2  28713  uspgr2wlkeq  28903  wwlks  29089  iswwlksnon  29107  rusgr0edg  29227  clwwlkccatlem  29242  clwwisshclwwslem  29267  clwwlkn  29279  clwwlknon  29343  3cyclfrgrrn  29539  vdgn1frgrv3  29550  2wspmdisj  29590  numclwlk2lem2f1o  29632  frgrregord013  29648  htthlem  30170  ocsh  30536  shintcli  30582  pjss2coi  31417  pjnormssi  31421  pjclem4  31452  pj3si  31460  pj3cor1i  31462  strlem3a  31505  strb  31511  hstrlem3a  31513  hstrbi  31519  spansncv2  31546  mdsl1i  31574  cvmdi  31577  mdexchi  31588  h1da  31602  mdsymlem6  31661  sumdmdii  31668  dmdbr5ati  31675  isoun  31923  supssd  31934  infssd  31935  xrge0tsmsd  32209  ordtrest2NEW  32903  pwsiga  33128  measiun  33216  dya2iocuni  33282  bnj518  33897  bnj1137  34006  bnj1136  34008  bnj1413  34046  bnj1417  34052  bnj60  34073  subgrwlk  34123  erdszelem8  34189  cvmsss2  34265  cvmfolem  34270  fmlasucdisj  34390  satfun  34402  dfon2lem8  34762  dfon2lem9  34763  dfon2  34764  rdgprc  34766  nn0prpwlem  35207  ntruni  35212  clsint2  35214  fneint  35233  fnessref  35242  refssfne  35243  neibastop1  35244  neibastop2lem  35245  bj-0int  35982  bj-ismooredr  35990  relowlpssretop  36245  fvineqsneu  36292  fvineqsneq  36293  heicant  36523  mblfinlem1  36525  ftc2nc  36570  sdclem2  36610  fdc  36613  seqpo  36615  prdsbnd  36661  heibor  36689  rrnequiv  36703  0idl  36893  intidl  36897  unichnidl  36899  prnc  36935  uniqsALTV  37198  refressn  37313  lsmcv2  37899  lcvexchlem4  37907  lcvexchlem5  37908  eqlkr  37969  paddclN  38713  pclfinN  38771  ldilcnv  38986  ldilco  38987  cdleme25dN  39227  cdlemj2  39693  tendocan  39695  erng1lem  39858  erngdvlem4-rN  39870  dihord2pre  40096  dihglblem2N  40165  dochvalr  40228  hdmap14lem12  40750  hdmap14lem13  40751  fsuppind  41162  pellfundre  41619  pellfundge  41620  pellfundlb  41622  dford3lem1  41765  aomclem2  41797  oaabsb  42044  cantnf2  42075  ofoafg  42104  naddcnff  42112  naddwordnexlem3  42150  naddwordnexlem4  42152  pwinfi3  42314  iunrelexp0  42453  iunrelexpmin1  42459  iunrelexpmin2  42463  dftrcl3  42471  cnvtrclfv  42475  trclimalb2  42477  dfrtrcl3  42484  ntrneiel2  42837  ntrneik4w  42851  ntrrn  42873  gneispa  42881  gneispb  42882  addrcom  43234  iunconnlem2  43696  ssuzfz  44059  dvmptfprod  44661  dvnprodlem3  44664  funressnfv  45753  cfsetsnfsetfo  45770  tz6.12-afv  45881  tz6.12-afv2  45948  otiunsndisjX  45987  uniimaprimaeqfv  46050  iccpartltu  46093  iccpartgtl  46094  iccpartleu  46096  iccpartgel  46097  fargshiftf  46108  fargshiftfva  46111  sbgoldbst  46446  bgoldbtbnd  46477  tgblthelfgott  46483  isomushgr  46494  nnsgrp  46587  pzriprnglem4  46808  pzriprnglem7  46811  pzriprnglem13  46817  ellcoellss  47116  lindsrng01  47149  suppdm  47191  nn0sumshdiglem1  47307  setrec2fun  47737