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  elirrv  9525  wemapwe  9626  ttrclss  9649  trcl  9657  frr3g  9685  tz9.13  9720  rankval3b  9755  rankunb  9779  rankuni2b  9782  scott0  9815  updjud  9863  dfac8alem  9958  carduniima  10025  alephsmo  10031  alephval3  10039  iunfictbso  10043  dfac3  10050  dfac5lem5  10056  dfac12r  10076  dfac12k  10077  kmlem4  10083  kmlem11  10090  cfsuc  10186  cofsmo  10198  cfsmolem  10199  coftr  10202  alephsing  10205  infpssrlem3  10234  fin23lem30  10271  isf32lem2  10283  isf32lem3  10284  isf34lem6  10309  fin1a2lem11  10339  fin1a2lem13  10341  fin1a2s  10343  axcc2lem  10365  domtriomlem  10371  axdc3lem2  10380  axdc4lem  10384  axcclem  10386  axdclem2  10449  iundom2g  10469  uniimadom  10473  cardmin  10493  alephval2  10501  alephreg  10511  fpwwe2lem11  10570  wunex2  10667  wuncval2  10676  tskwe2  10702  inar1  10704  tskuni  10712  gruun  10735  intgru  10743  grutsk1  10750  genpcl  10937  ltexprlem5  10969  suplem1pr  10981  supexpr  10983  supsrlem  11040  axpre-sup  11098  negfi  12108  supaddc  12126  supadd  12127  supmul1  12128  supmullem1  12129  supmul  12131  peano5nni  12165  uzind  12602  zindd  12611  uzwo  12846  lbzbi  12871  xrsupsslem  13243  xrinfmsslem  13244  supxrun  13252  supxrpnf  13254  supxrunb1  13255  supxrunb2  13256  icoshftf1o  13411  flval3  13753  axdc4uzlem  13924  tpfo  14441  wrdnfi  14489  ccatrn  14530  ccatalpha  14534  2cshw  14754  cshweqrep  14762  s3iunsndisj  14910  rtrclreclem4  15003  dfrtrcl2  15004  01sqrexlem1  15184  01sqrexlem6  15189  fsum0diag2  15725  alzdvds  16266  gcdcllem1  16445  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  maxprmfct  16655  hashgcdeq  16736  unbenlem  16855  vdwlem6  16933  vdwlem10  16937  firest  17371  mrieqv2d  17580  iscatd  17614  initoeu2  17958  setcmon  18029  setcepi  18030  fullestrcsetc  18092  fullsetcestrc  18107  isglbd  18450  isacs4lem  18485  acsfiindd  18494  acsmapd  18495  psss  18521  sgrpidmnd  18648  pwmnd  18846  ghmrn  19143  ghmpreima  19152  cntz2ss  19249  symgextres  19339  psgnunilem2  19409  lsmsubg  19568  efgsfo  19653  gsumzaddlem  19835  gsummptnn0fzfv  19901  dmdprdd  19915  dprd2da  19958  ablsimpgprmd  20031  imasring  20250  01eq0ring  20450  isabvd  20732  issrngd  20775  islssd  20873  lbsextlem3  21102  lbsextlem4  21103  lidldvgen  21276  pzriprnglem4  21426  pzriprnglem7  21429  pzriprnglem13  21435  psgnghm  21522  isphld  21596  frlmsslsp  21738  mp2pm2mplem4  22729  tgcl  22889  distop  22915  indistopon  22921  pptbas  22928  toponmre  23013  opnnei  23040  neiuni  23042  neindisj2  23043  ordtrest2  23124  cnpnei  23184  cnindis  23212  cmpcld  23322  uncmp  23323  hauscmplem  23326  2ndc1stc  23371  1stcrest  23373  1stcelcls  23381  llyrest  23405  nllyrest  23406  cldllycmp  23415  reftr  23434  locfincf  23451  comppfsc  23452  txcls  23524  ptpjcn  23531  ptclsg  23535  dfac14lem  23537  xkoccn  23539  txlly  23556  txnlly  23557  ptrescn  23559  tx1stc  23570  xkoco1cn  23577  xkoco2cn  23578  xkococn  23580  xkoinjcn  23607  qtopeu  23636  hmeofval  23678  ordthmeolem  23721  isfild  23778  fbasrn  23804  trfil2  23807  flimclslem  23904  fclsrest  23944  fclscf  23945  flimfcls  23946  alexsubALTlem1  23967  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALT  23971  qustgpopn  24040  isxmetd  24247  imasdsf1olem  24294  blcls  24427  prdsxmslem2  24450  metustfbas  24478  dscmet  24493  nrmmetd  24495  reperflem  24740  reconnlem2  24749  xrge0tsms  24756  fsumcn  24794  cnheibor  24887  tcphcph  25170  lmmbr  25191  caubl  25241  ivthlem1  25385  ovolctb  25424  ovoliunlem2  25437  ovolscalem1  25447  ovolicc2  25456  voliunlem3  25486  ismbfd  25573  mbfimaopnlem  25589  itg2le  25673  ellimc2  25811  c1liplem1  25934  plyeq0lem  26148  dgreq0  26204  aannenlem1  26269  pilem2  26395  cxpcn3lem  26690  scvxcvx  26929  musum  27134  fsumdvdsmul  27138  dchrisum0flb  27454  ostth2lem2  27578  sltval2  27601  nolesgn2ores  27617  nogesgn1ores  27619  nosupres  27652  nosupbnd2lem1  27660  noinfres  27667  noinfbnd2lem1  27675  scutun12  27756  madebdayim  27837  precsexlem9  28157  noseqind  28226  zs12zodd  28394  zs12bday  28396  numedglnl  29124  upgrreslem  29284  umgrreslem  29285  nbuhgr  29323  nbumgr  29327  uhgrnbgr0nb  29334  nbusgrf1o0  29349  uvtxnbgrvtx  29373  cusgrfilem2  29437  uspgr2wlkeq  29626  wwlks  29815  iswwlksnon  29833  rusgr0edg  29953  clwwlkccatlem  29968  clwwisshclwwslem  29993  clwwlkn  30005  clwwlknon  30069  3cyclfrgrrn  30265  vdgn1frgrv3  30276  2wspmdisj  30316  numclwlk2lem2f1o  30358  frgrregord013  30374  htthlem  30896  ocsh  31262  shintcli  31308  pjss2coi  32143  pjnormssi  32147  pjclem4  32178  pj3si  32186  pj3cor1i  32188  strlem3a  32231  strb  32237  hstrlem3a  32239  hstrbi  32245  spansncv2  32272  mdsl1i  32300  cvmdi  32303  mdexchi  32314  h1da  32328  mdsymlem6  32387  sumdmdii  32394  dmdbr5ati  32401  isoun  32675  xrge0tsmsd  33045  ordtrest2NEW  33906  pwsiga  34113  measiun  34201  dya2iocuni  34267  bnj518  34869  bnj1137  34978  bnj1136  34980  bnj1413  35018  bnj1417  35024  bnj60  35045  gblacfnacd  35082  onvf1odlem1  35083  onvf1odlem4  35086  subgrwlk  35112  erdszelem8  35178  cvmsss2  35254  cvmfolem  35259  fmlasucdisj  35379  satfun  35391  dfon2lem8  35771  dfon2lem9  35772  dfon2  35773  rdgprc  35775  nn0prpwlem  36303  ntruni  36308  clsint2  36310  fneint  36329  fnessref  36338  refssfne  36339  neibastop1  36340  neibastop2lem  36341  bj-0int  37082  bj-ismooredr  37090  relowlpssretop  37345  fvineqsneu  37392  fvineqsneq  37393  heicant  37642  mblfinlem1  37644  ftc2nc  37689  sdclem2  37729  fdc  37732  seqpo  37734  prdsbnd  37780  heibor  37808  rrnequiv  37822  0idl  38012  intidl  38016  unichnidl  38018  prnc  38054  refressn  38427  lsmcv2  39015  lcvexchlem4  39023  lcvexchlem5  39024  eqlkr  39085  paddclN  39829  pclfinN  39887  ldilcnv  40102  ldilco  40103  cdleme25dN  40343  cdlemj2  40809  tendocan  40811  erng1lem  40974  erngdvlem4-rN  40986  dihord2pre  41212  dihglblem2N  41281  dochvalr  41344  hdmap14lem12  41866  hdmap14lem13  41867  supinf  42223  fsuppind  42571  pellfundre  42862  pellfundge  42863  pellfundlb  42865  dford3lem1  43008  aomclem2  43037  oaabsb  43276  cantnf2  43307  ofoafg  43336  naddcnff  43344  naddwordnexlem3  43381  naddwordnexlem4  43383  pwinfi3  43545  iunrelexp0  43684  iunrelexpmin1  43690  iunrelexpmin2  43694  dftrcl3  43702  cnvtrclfv  43706  trclimalb2  43708  dfrtrcl3  43715  ntrneiel2  44068  ntrneik4w  44082  ntrrn  44104  gneispa  44112  gneispb  44113  addrcom  44457  iunconnlem2  44917  ssuzfz  45338  dvnprodlem3  45939  funressnfv  47037  cfsetsnfsetfo  47054  tz6.12-afv  47167  tz6.12-afv2  47234  otiunsndisjX  47273  uniimaprimaeqfv  47376  iccpartltu  47419  iccpartgtl  47420  iccpartleu  47422  iccpartgel  47423  fargshiftf  47434  fargshiftfva  47437  sbgoldbst  47772  bgoldbtbnd  47803  tgblthelfgott  47809  grimuhgr  47880  grimco  47882  isuspgrim0  47887  isuspgrimlem  47888  upgrimpths  47902  gricushgr  47910  grtriclwlk3  47937  stgr0  47952  uspgrlim  47984  grlicsym  47998  nnsgrp  48158  ellcoellss  48417  lindsrng01  48450  suppdm  48492  nn0sumshdiglem1  48603  setrec2fun  49674