Theorem ralrimiv 3129

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  ralrimiva  3130  ralrimivw  3134  ralrimdv  3136  ralrimivv  3179  rr19.3v  3610  class2seteq  3651  rabssdv  4015  rzalALT  4436  r19.3rzv  4444  disjord  5075  disjiund  5077  trun  5204  trin  5205  ralxfrALT  5354  otiunsndisj  5470  onmindif  6413  fnprb  7158  fntpb  7159  f1cdmsn  7232  ssorduni  7728  onminex  7751  onmindif2  7756  limuni3  7798  frxp  8071  poxp  8073  sexp2  8091  sexp3  8098  onfununi  8276  onnseq  8279  tfrlem12  8323  tz7.48-2  8376  oaass  8491  omass  8510  oelim2  8526  oelimcl  8531  oaabs2  8580  omabs  8582  uniqs  8715  undifixp  8877  dom2lem  8934  isinf  9170  unblem4  9200  unbnn2  9202  marypha1lem  9341  supssd  9371  supiso  9384  infssd  9402  ordiso2  9425  card2inf  9465  elirrvOLD  9508  wemapwe  9613  ttrclss  9636  trcl  9644  frr3g  9675  tz9.13  9710  rankval3b  9745  rankunb  9769  rankuni2b  9772  scott0  9805  updjud  9853  dfac8alem  9946  carduniima  10013  alephsmo  10019  alephval3  10027  iunfictbso  10031  dfac3  10038  dfac5lem5  10044  dfac12r  10064  dfac12k  10065  kmlem4  10071  kmlem11  10078  cfsuc  10174  cofsmo  10186  cfsmolem  10187  coftr  10190  alephsing  10193  infpssrlem3  10222  fin23lem30  10259  isf32lem2  10271  isf32lem3  10272  isf34lem6  10297  fin1a2lem11  10327  fin1a2lem13  10329  fin1a2s  10331  axcc2lem  10353  domtriomlem  10359  axdc3lem2  10368  axdc4lem  10372  axcclem  10374  axdclem2  10437  iundom2g  10457  uniimadom  10461  cardmin  10481  alephval2  10490  alephreg  10500  fpwwe2lem11  10559  wunex2  10656  wuncval2  10665  tskwe2  10691  inar1  10693  tskuni  10701  gruun  10724  intgru  10732  grutsk1  10739  genpcl  10926  ltexprlem5  10958  suplem1pr  10970  supexpr  10972  supsrlem  11029  axpre-sup  11087  negfi  12100  supaddc  12118  supadd  12119  supmul1  12120  supmullem1  12121  supmul  12123  peano5nni  12172  uzind  12616  zindd  12625  uzwo  12856  lbzbi  12881  xrsupsslem  13254  xrinfmsslem  13255  supxrun  13263  supxrpnf  13265  supxrunb1  13266  supxrunb2  13267  icoshftf1o  13422  flval3  13769  axdc4uzlem  13940  tpfo  14457  wrdnfi  14505  ccatrn  14547  ccatalpha  14551  2cshw  14770  cshweqrep  14778  s3iunsndisj  14925  rtrclreclem4  15018  dfrtrcl2  15019  01sqrexlem1  15199  01sqrexlem6  15204  fsum0diag2  15740  alzdvds  16284  gcdcllem1  16463  lcmfunsnlem2lem1  16602  lcmfunsnlem2lem2  16603  maxprmfct  16674  hashgcdeq  16755  unbenlem  16874  vdwlem6  16952  vdwlem10  16956  firest  17390  mrieqv2d  17600  iscatd  17634  initoeu2  17978  setcmon  18049  setcepi  18050  fullestrcsetc  18112  fullsetcestrc  18127  isglbd  18470  isacs4lem  18505  acsfiindd  18514  acsmapd  18515  psss  18541  sgrpidmnd  18702  pwmnd  18903  ghmrn  19199  ghmpreima  19208  cntz2ss  19305  symgextres  19395  psgnunilem2  19465  lsmsubg  19624  efgsfo  19709  gsumzaddlem  19891  gsummptnn0fzfv  19957  dmdprdd  19971  dprd2da  20014  ablsimpgprmd  20087  imasring  20305  01eq0ring  20502  isabvd  20784  issrngd  20827  islssd  20925  lbsextlem3  21154  lbsextlem4  21155  lidldvgen  21328  pzriprnglem4  21478  pzriprnglem7  21481  pzriprnglem13  21487  psgnghm  21574  isphld  21648  frlmsslsp  21790  mp2pm2mplem4  22788  tgcl  22948  distop  22974  indistopon  22980  pptbas  22987  toponmre  23072  opnnei  23099  neiuni  23101  neindisj2  23102  ordtrest2  23183  cnpnei  23243  cnindis  23271  cmpcld  23381  uncmp  23382  hauscmplem  23385  2ndc1stc  23430  1stcrest  23432  1stcelcls  23440  llyrest  23464  nllyrest  23465  cldllycmp  23474  reftr  23493  locfincf  23510  comppfsc  23511  txcls  23583  ptpjcn  23590  ptclsg  23594  dfac14lem  23596  xkoccn  23598  txlly  23615  txnlly  23616  ptrescn  23618  tx1stc  23629  xkoco1cn  23636  xkoco2cn  23637  xkococn  23639  xkoinjcn  23666  qtopeu  23695  hmeofval  23737  ordthmeolem  23780  isfild  23837  fbasrn  23863  trfil2  23866  flimclslem  23963  fclsrest  24003  fclscf  24004  flimfcls  24005  alexsubALTlem1  24026  alexsubALTlem2  24027  alexsubALTlem3  24028  alexsubALT  24030  qustgpopn  24099  isxmetd  24305  imasdsf1olem  24352  blcls  24485  prdsxmslem2  24508  metustfbas  24536  dscmet  24551  nrmmetd  24553  reperflem  24798  reconnlem2  24807  xrge0tsms  24814  fsumcn  24851  cnheibor  24936  tcphcph  25218  lmmbr  25239  caubl  25289  ivthlem1  25432  ovolctb  25471  ovoliunlem2  25484  ovolscalem1  25494  ovolicc2  25503  voliunlem3  25533  ismbfd  25620  mbfimaopnlem  25636  itg2le  25720  ellimc2  25858  c1liplem1  25977  plyeq0lem  26189  dgreq0  26244  aannenlem1  26309  pilem2  26434  cxpcn3lem  26728  scvxcvx  26967  musum  27172  fsumdvdsmul  27176  dchrisum0flb  27491  ostth2lem2  27615  ltsval2  27638  nolesgn2ores  27654  nogesgn1ores  27656  nosupres  27689  nosupbnd2lem1  27697  noinfres  27704  noinfbnd2lem1  27712  cutsun12  27800  madebdayim  27898  precsexlem9  28225  addonbday  28289  noseqind  28302  z12zsodd  28492  numedglnl  29231  upgrreslem  29391  umgrreslem  29392  nbuhgr  29430  nbumgr  29434  uhgrnbgr0nb  29441  nbusgrf1o0  29456  uvtxnbgrvtx  29480  cusgrfilem2  29544  uspgr2wlkeq  29733  wwlks  29922  iswwlksnon  29940  rusgr0edg  30063  clwwlkccatlem  30078  clwwisshclwwslem  30103  clwwlkn  30115  clwwlknon  30179  3cyclfrgrrn  30375  vdgn1frgrv3  30386  2wspmdisj  30426  numclwlk2lem2f1o  30468  frgrregord013  30484  htthlem  31007  ocsh  31373  shintcli  31419  pjss2coi  32254  pjnormssi  32258  pjclem4  32289  pj3si  32297  pj3cor1i  32299  strlem3a  32342  strb  32348  hstrlem3a  32350  hstrbi  32356  spansncv2  32383  mdsl1i  32411  cvmdi  32414  mdexchi  32425  h1da  32439  mdsymlem6  32498  sumdmdii  32505  dmdbr5ati  32512  isoun  32794  xrge0tsmsd  33153  ordtrest2NEW  34087  pwsiga  34294  measiun  34382  dya2iocuni  34447  bnj518  35048  bnj1137  35157  bnj1136  35159  bnj1413  35197  bnj1417  35203  bnj60  35224  rankval4b  35263  r1filim  35267  trssfir1om  35275  fineqvnttrclselem3  35287  fineqvinfep  35289  tz9.1regs  35298  trssfir1omregs  35300  gblacfnacd  35304  onvf1odlem1  35305  onvf1odlem4  35308  subgrwlk  35334  erdszelem8  35400  cvmsss2  35476  cvmfolem  35481  fmlasucdisj  35601  satfun  35613  dfon2lem8  35990  dfon2lem9  35991  dfon2  35992  rdgprc  35994  nn0prpwlem  36524  ntruni  36529  clsint2  36531  fneint  36550  fnessref  36559  refssfne  36560  neibastop1  36561  neibastop2lem  36562  mh-inf3f1  36743  bj-0int  37433  bj-ismooredr  37441  relowlpssretop  37700  fvineqsneu  37747  fvineqsneq  37748  heicant  37996  mblfinlem1  37998  ftc2nc  38043  sdclem2  38083  fdc  38086  seqpo  38088  prdsbnd  38134  heibor  38162  rrnequiv  38176  0idl  38366  intidl  38370  unichnidl  38372  prnc  38408  refressn  38874  lsmcv2  39495  lcvexchlem4  39503  lcvexchlem5  39504  eqlkr  39565  paddclN  40308  pclfinN  40366  ldilcnv  40581  ldilco  40582  cdleme25dN  40822  cdlemj2  41288  tendocan  41290  erng1lem  41453  erngdvlem4-rN  41465  dihord2pre  41691  dihglblem2N  41760  dochvalr  41823  hdmap14lem12  42345  hdmap14lem13  42346  supinf  42701  fsuppind  43043  pellfundre  43333  pellfundge  43334  pellfundlb  43336  dford3lem1  43478  aomclem2  43507  oaabsb  43746  cantnf2  43777  ofoafg  43806  naddcnff  43814  naddwordnexlem3  43851  naddwordnexlem4  43853  pwinfi3  44014  iunrelexp0  44153  iunrelexpmin1  44159  iunrelexpmin2  44163  dftrcl3  44171  cnvtrclfv  44175  trclimalb2  44177  dfrtrcl3  44184  ntrneiel2  44537  ntrneik4w  44551  ntrrn  44573  gneispa  44581  gneispb  44582  addrcom  44925  iunconnlem2  45385  ssuzfz  45803  dvnprodlem3  46400  funressnfv  47509  cfsetsnfsetfo  47526  tz6.12-afv  47639  tz6.12-afv2  47706  otiunsndisjX  47745  uniimaprimaeqfv  47860  iccpartltu  47903  iccpartgtl  47904  iccpartleu  47906  iccpartgel  47907  fargshiftf  47918  fargshiftfva  47921  sbgoldbst  48272  bgoldbtbnd  48303  tgblthelfgott  48309  grimuhgr  48381  grimco  48383  isuspgrim0  48388  isuspgrimlem  48389  upgrimpths  48403  gricushgr  48411  grtriclwlk3  48439  stgr0  48454  uspgrlim  48486  grlicsym  48507  nnsgrp  48671  ellcoellss  48929  lindsrng01  48962  suppdm  49004  nn0sumshdiglem1  49115  setrec2fun  50185