Theorem ralrimiv 3124

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralrimiva  3125  ralrimivw  3129  ralrimdv  3131  ralrimivv  3176  rr19.3v  3630  class2seteq  3672  rabssdv  4034  rzalALT  4469  disjord  5091  disjiund  5093  trin  5221  ralxfrALT  5365  otiunsndisj  5475  onmindif  6414  fnprb  7164  fntpb  7165  f1cdmsn  7239  ssorduni  7735  onminex  7758  onmindif2  7763  sucexeloniOLD  7766  limuni3  7808  frxp  8082  poxp  8084  sexp2  8102  sexp3  8109  onfununi  8287  onnseq  8290  tfrlem12  8334  tz7.48-2  8387  oaass  8502  omass  8521  oelim2  8536  oelimcl  8541  oaabs2  8590  omabs  8592  uniqs  8724  undifixp  8884  dom2lem  8940  isinf  9183  isinfOLD  9184  unblem4  9218  unbnn2  9220  marypha1lem  9360  supssd  9390  supiso  9403  infssd  9421  ordiso2  9444  card2inf  9484  elirrvOLD  9526  wemapwe  9628  ttrclss  9651  trcl  9659  frr3g  9687  tz9.13  9722  rankval3b  9757  rankunb  9781  rankuni2b  9784  scott0  9817  updjud  9865  dfac8alem  9960  carduniima  10027  alephsmo  10033  alephval3  10041  iunfictbso  10045  dfac3  10052  dfac5lem5  10058  dfac12r  10078  dfac12k  10079  kmlem4  10085  kmlem11  10092  cfsuc  10188  cofsmo  10200  cfsmolem  10201  coftr  10204  alephsing  10207  infpssrlem3  10236  fin23lem30  10273  isf32lem2  10285  isf32lem3  10286  isf34lem6  10311  fin1a2lem11  10341  fin1a2lem13  10343  fin1a2s  10345  axcc2lem  10367  domtriomlem  10373  axdc3lem2  10382  axdc4lem  10386  axcclem  10388  axdclem2  10451  iundom2g  10471  uniimadom  10475  cardmin  10495  alephval2  10503  alephreg  10513  fpwwe2lem11  10572  wunex2  10669  wuncval2  10678  tskwe2  10704  inar1  10706  tskuni  10714  gruun  10737  intgru  10745  grutsk1  10752  genpcl  10939  ltexprlem5  10971  suplem1pr  10983  supexpr  10985  supsrlem  11042  axpre-sup  11100  negfi  12110  supaddc  12128  supadd  12129  supmul1  12130  supmullem1  12131  supmul  12133  peano5nni  12167  uzind  12604  zindd  12613  uzwo  12848  lbzbi  12873  xrsupsslem  13245  xrinfmsslem  13246  supxrun  13254  supxrpnf  13256  supxrunb1  13257  supxrunb2  13258  icoshftf1o  13413  flval3  13755  axdc4uzlem  13926  tpfo  14443  wrdnfi  14491  ccatrn  14532  ccatalpha  14536  2cshw  14755  cshweqrep  14763  s3iunsndisj  14911  rtrclreclem4  15004  dfrtrcl2  15005  01sqrexlem1  15185  01sqrexlem6  15190  fsum0diag2  15726  alzdvds  16267  gcdcllem1  16446  lcmfunsnlem2lem1  16585  lcmfunsnlem2lem2  16586  maxprmfct  16656  hashgcdeq  16737  unbenlem  16856  vdwlem6  16934  vdwlem10  16938  firest  17372  mrieqv2d  17581  iscatd  17615  initoeu2  17959  setcmon  18030  setcepi  18031  fullestrcsetc  18093  fullsetcestrc  18108  isglbd  18451  isacs4lem  18486  acsfiindd  18495  acsmapd  18496  psss  18522  sgrpidmnd  18649  pwmnd  18847  ghmrn  19144  ghmpreima  19153  cntz2ss  19250  symgextres  19340  psgnunilem2  19410  lsmsubg  19569  efgsfo  19654  gsumzaddlem  19836  gsummptnn0fzfv  19902  dmdprdd  19916  dprd2da  19959  ablsimpgprmd  20032  imasring  20251  01eq0ring  20451  isabvd  20733  issrngd  20776  islssd  20874  lbsextlem3  21103  lbsextlem4  21104  lidldvgen  21277  pzriprnglem4  21427  pzriprnglem7  21430  pzriprnglem13  21436  psgnghm  21523  isphld  21597  frlmsslsp  21739  mp2pm2mplem4  22730  tgcl  22890  distop  22916  indistopon  22922  pptbas  22929  toponmre  23014  opnnei  23041  neiuni  23043  neindisj2  23044  ordtrest2  23125  cnpnei  23185  cnindis  23213  cmpcld  23323  uncmp  23324  hauscmplem  23327  2ndc1stc  23372  1stcrest  23374  1stcelcls  23382  llyrest  23406  nllyrest  23407  cldllycmp  23416  reftr  23435  locfincf  23452  comppfsc  23453  txcls  23525  ptpjcn  23532  ptclsg  23536  dfac14lem  23538  xkoccn  23540  txlly  23557  txnlly  23558  ptrescn  23560  tx1stc  23571  xkoco1cn  23578  xkoco2cn  23579  xkococn  23581  xkoinjcn  23608  qtopeu  23637  hmeofval  23679  ordthmeolem  23722  isfild  23779  fbasrn  23805  trfil2  23808  flimclslem  23905  fclsrest  23945  fclscf  23946  flimfcls  23947  alexsubALTlem1  23968  alexsubALTlem2  23969  alexsubALTlem3  23970  alexsubALT  23972  qustgpopn  24041  isxmetd  24248  imasdsf1olem  24295  blcls  24428  prdsxmslem2  24451  metustfbas  24479  dscmet  24494  nrmmetd  24496  reperflem  24741  reconnlem2  24750  xrge0tsms  24757  fsumcn  24795  cnheibor  24888  tcphcph  25171  lmmbr  25192  caubl  25242  ivthlem1  25386  ovolctb  25425  ovoliunlem2  25438  ovolscalem1  25448  ovolicc2  25457  voliunlem3  25487  ismbfd  25574  mbfimaopnlem  25590  itg2le  25674  ellimc2  25812  c1liplem1  25935  plyeq0lem  26149  dgreq0  26205  aannenlem1  26270  pilem2  26396  cxpcn3lem  26691  scvxcvx  26930  musum  27135  fsumdvdsmul  27139  dchrisum0flb  27455  ostth2lem2  27579  sltval2  27602  nolesgn2ores  27618  nogesgn1ores  27620  nosupres  27653  nosupbnd2lem1  27661  noinfres  27668  noinfbnd2lem1  27676  scutun12  27757  madebdayim  27838  precsexlem9  28158  noseqind  28227  zs12zodd  28395  zs12bday  28397  numedglnl  29125  upgrreslem  29285  umgrreslem  29286  nbuhgr  29324  nbumgr  29328  uhgrnbgr0nb  29335  nbusgrf1o0  29350  uvtxnbgrvtx  29374  cusgrfilem2  29438  uspgr2wlkeq  29627  wwlks  29816  iswwlksnon  29834  rusgr0edg  29954  clwwlkccatlem  29969  clwwisshclwwslem  29994  clwwlkn  30006  clwwlknon  30070  3cyclfrgrrn  30266  vdgn1frgrv3  30277  2wspmdisj  30317  numclwlk2lem2f1o  30359  frgrregord013  30375  htthlem  30897  ocsh  31263  shintcli  31309  pjss2coi  32144  pjnormssi  32148  pjclem4  32179  pj3si  32187  pj3cor1i  32189  strlem3a  32232  strb  32238  hstrlem3a  32240  hstrbi  32246  spansncv2  32273  mdsl1i  32301  cvmdi  32304  mdexchi  32315  h1da  32329  mdsymlem6  32388  sumdmdii  32395  dmdbr5ati  32402  isoun  32676  xrge0tsmsd  33046  ordtrest2NEW  33907  pwsiga  34114  measiun  34202  dya2iocuni  34268  bnj518  34870  bnj1137  34979  bnj1136  34981  bnj1413  35019  bnj1417  35025  bnj60  35046  gblacfnacd  35083  onvf1odlem1  35084  onvf1odlem4  35087  subgrwlk  35113  erdszelem8  35179  cvmsss2  35255  cvmfolem  35260  fmlasucdisj  35380  satfun  35392  dfon2lem8  35772  dfon2lem9  35773  dfon2  35774  rdgprc  35776  nn0prpwlem  36304  ntruni  36309  clsint2  36311  fneint  36330  fnessref  36339  refssfne  36340  neibastop1  36341  neibastop2lem  36342  bj-0int  37083  bj-ismooredr  37091  relowlpssretop  37346  fvineqsneu  37393  fvineqsneq  37394  heicant  37643  mblfinlem1  37645  ftc2nc  37690  sdclem2  37730  fdc  37733  seqpo  37735  prdsbnd  37781  heibor  37809  rrnequiv  37823  0idl  38013  intidl  38017  unichnidl  38019  prnc  38055  refressn  38428  lsmcv2  39016  lcvexchlem4  39024  lcvexchlem5  39025  eqlkr  39086  paddclN  39830  pclfinN  39888  ldilcnv  40103  ldilco  40104  cdleme25dN  40344  cdlemj2  40810  tendocan  40812  erng1lem  40975  erngdvlem4-rN  40987  dihord2pre  41213  dihglblem2N  41282  dochvalr  41345  hdmap14lem12  41867  hdmap14lem13  41868  supinf  42224  fsuppind  42572  pellfundre  42863  pellfundge  42864  pellfundlb  42866  dford3lem1  43009  aomclem2  43038  oaabsb  43277  cantnf2  43308  ofoafg  43337  naddcnff  43345  naddwordnexlem3  43382  naddwordnexlem4  43384  pwinfi3  43546  iunrelexp0  43685  iunrelexpmin1  43691  iunrelexpmin2  43695  dftrcl3  43703  cnvtrclfv  43707  trclimalb2  43709  dfrtrcl3  43716  ntrneiel2  44069  ntrneik4w  44083  ntrrn  44105  gneispa  44113  gneispb  44114  addrcom  44458  iunconnlem2  44918  ssuzfz  45339  dvnprodlem3  45940  funressnfv  47038  cfsetsnfsetfo  47055  tz6.12-afv  47168  tz6.12-afv2  47235  otiunsndisjX  47274  uniimaprimaeqfv  47377  iccpartltu  47420  iccpartgtl  47421  iccpartleu  47423  iccpartgel  47424  fargshiftf  47435  fargshiftfva  47438  sbgoldbst  47773  bgoldbtbnd  47804  tgblthelfgott  47810  grimuhgr  47881  grimco  47883  isuspgrim0  47888  isuspgrimlem  47889  upgrimpths  47903  gricushgr  47911  grtriclwlk3  47938  stgr0  47953  uspgrlim  47985  grlicsym  47999  nnsgrp  48159  ellcoellss  48418  lindsrng01  48451  suppdm  48493  nn0sumshdiglem1  48604  setrec2fun  49675