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  3623  class2seteq  3664  rabssdv  4028  rzalALT  4450  r19.3rzv  4458  disjord  5089  disjiund  5091  trin  5218  ralxfrALT  5364  otiunsndisj  5478  onmindif  6421  fnprb  7166  fntpb  7167  f1cdmsn  7240  ssorduni  7736  onminex  7759  onmindif2  7764  limuni3  7806  frxp  8080  poxp  8082  sexp2  8100  sexp3  8107  onfununi  8285  onnseq  8288  tfrlem12  8332  tz7.48-2  8385  oaass  8500  omass  8519  oelim2  8535  oelimcl  8540  oaabs2  8589  omabs  8591  uniqs  8724  undifixp  8886  dom2lem  8943  isinf  9179  unblem4  9209  unbnn2  9211  marypha1lem  9350  supssd  9380  supiso  9393  infssd  9411  ordiso2  9434  card2inf  9474  elirrvOLD  9517  wemapwe  9620  ttrclss  9643  trcl  9651  frr3g  9682  tz9.13  9717  rankval3b  9752  rankunb  9776  rankuni2b  9779  scott0  9812  updjud  9860  dfac8alem  9953  carduniima  10020  alephsmo  10026  alephval3  10034  iunfictbso  10038  dfac3  10045  dfac5lem5  10051  dfac12r  10071  dfac12k  10072  kmlem4  10078  kmlem11  10085  cfsuc  10181  cofsmo  10193  cfsmolem  10194  coftr  10197  alephsing  10200  infpssrlem3  10229  fin23lem30  10266  isf32lem2  10278  isf32lem3  10279  isf34lem6  10304  fin1a2lem11  10334  fin1a2lem13  10336  fin1a2s  10338  axcc2lem  10360  domtriomlem  10366  axdc3lem2  10375  axdc4lem  10379  axcclem  10381  axdclem2  10444  iundom2g  10464  uniimadom  10468  cardmin  10488  alephval2  10497  alephreg  10507  fpwwe2lem11  10566  wunex2  10663  wuncval2  10672  tskwe2  10698  inar1  10700  tskuni  10708  gruun  10731  intgru  10739  grutsk1  10746  genpcl  10933  ltexprlem5  10965  suplem1pr  10977  supexpr  10979  supsrlem  11036  axpre-sup  11094  negfi  12105  supaddc  12123  supadd  12124  supmul1  12125  supmullem1  12126  supmul  12128  peano5nni  12162  uzind  12598  zindd  12607  uzwo  12838  lbzbi  12863  xrsupsslem  13236  xrinfmsslem  13237  supxrun  13245  supxrpnf  13247  supxrunb1  13248  supxrunb2  13249  icoshftf1o  13404  flval3  13749  axdc4uzlem  13920  tpfo  14437  wrdnfi  14485  ccatrn  14527  ccatalpha  14531  2cshw  14750  cshweqrep  14758  s3iunsndisj  14905  rtrclreclem4  14998  dfrtrcl2  14999  01sqrexlem1  15179  01sqrexlem6  15184  fsum0diag2  15720  alzdvds  16261  gcdcllem1  16440  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  maxprmfct  16650  hashgcdeq  16731  unbenlem  16850  vdwlem6  16928  vdwlem10  16932  firest  17366  mrieqv2d  17576  iscatd  17610  initoeu2  17954  setcmon  18025  setcepi  18026  fullestrcsetc  18088  fullsetcestrc  18103  isglbd  18446  isacs4lem  18481  acsfiindd  18490  acsmapd  18491  psss  18517  sgrpidmnd  18678  pwmnd  18879  ghmrn  19175  ghmpreima  19184  cntz2ss  19281  symgextres  19371  psgnunilem2  19441  lsmsubg  19600  efgsfo  19685  gsumzaddlem  19867  gsummptnn0fzfv  19933  dmdprdd  19947  dprd2da  19990  ablsimpgprmd  20063  imasring  20283  01eq0ring  20480  isabvd  20762  issrngd  20805  islssd  20903  lbsextlem3  21132  lbsextlem4  21133  lidldvgen  21306  pzriprnglem4  21456  pzriprnglem7  21459  pzriprnglem13  21465  psgnghm  21552  isphld  21626  frlmsslsp  21768  mp2pm2mplem4  22770  tgcl  22930  distop  22956  indistopon  22962  pptbas  22969  toponmre  23054  opnnei  23081  neiuni  23083  neindisj2  23084  ordtrest2  23165  cnpnei  23225  cnindis  23253  cmpcld  23363  uncmp  23364  hauscmplem  23367  2ndc1stc  23412  1stcrest  23414  1stcelcls  23422  llyrest  23446  nllyrest  23447  cldllycmp  23456  reftr  23475  locfincf  23492  comppfsc  23493  txcls  23565  ptpjcn  23572  ptclsg  23576  dfac14lem  23578  xkoccn  23580  txlly  23597  txnlly  23598  ptrescn  23600  tx1stc  23611  xkoco1cn  23618  xkoco2cn  23619  xkococn  23621  xkoinjcn  23648  qtopeu  23677  hmeofval  23719  ordthmeolem  23762  isfild  23819  fbasrn  23845  trfil2  23848  flimclslem  23945  fclsrest  23985  fclscf  23986  flimfcls  23987  alexsubALTlem1  24008  alexsubALTlem2  24009  alexsubALTlem3  24010  alexsubALT  24012  qustgpopn  24081  isxmetd  24287  imasdsf1olem  24334  blcls  24467  prdsxmslem2  24490  metustfbas  24518  dscmet  24533  nrmmetd  24535  reperflem  24780  reconnlem2  24789  xrge0tsms  24796  fsumcn  24834  cnheibor  24927  tcphcph  25210  lmmbr  25231  caubl  25281  ivthlem1  25425  ovolctb  25464  ovoliunlem2  25477  ovolscalem1  25487  ovolicc2  25496  voliunlem3  25526  ismbfd  25613  mbfimaopnlem  25629  itg2le  25713  ellimc2  25851  c1liplem1  25974  plyeq0lem  26188  dgreq0  26244  aannenlem1  26309  pilem2  26435  cxpcn3lem  26730  scvxcvx  26969  musum  27174  fsumdvdsmul  27178  dchrisum0flb  27494  ostth2lem2  27618  ltsval2  27641  nolesgn2ores  27657  nogesgn1ores  27659  nosupres  27692  nosupbnd2lem1  27700  noinfres  27707  noinfbnd2lem1  27715  cutsun12  27803  madebdayim  27901  precsexlem9  28228  addonbday  28292  noseqind  28305  z12zsodd  28495  numedglnl  29235  upgrreslem  29395  umgrreslem  29396  nbuhgr  29434  nbumgr  29438  uhgrnbgr0nb  29445  nbusgrf1o0  29460  uvtxnbgrvtx  29484  cusgrfilem2  29548  uspgr2wlkeq  29737  wwlks  29926  iswwlksnon  29944  rusgr0edg  30067  clwwlkccatlem  30082  clwwisshclwwslem  30107  clwwlkn  30119  clwwlknon  30183  3cyclfrgrrn  30379  vdgn1frgrv3  30390  2wspmdisj  30430  numclwlk2lem2f1o  30472  frgrregord013  30488  htthlem  31011  ocsh  31377  shintcli  31423  pjss2coi  32258  pjnormssi  32262  pjclem4  32293  pj3si  32301  pj3cor1i  32303  strlem3a  32346  strb  32352  hstrlem3a  32354  hstrbi  32360  spansncv2  32387  mdsl1i  32415  cvmdi  32418  mdexchi  32429  h1da  32443  mdsymlem6  32502  sumdmdii  32509  dmdbr5ati  32516  isoun  32798  xrge0tsmsd  33173  ordtrest2NEW  34107  pwsiga  34314  measiun  34402  dya2iocuni  34467  bnj518  35068  bnj1137  35177  bnj1136  35179  bnj1413  35217  bnj1417  35223  bnj60  35244  rankval4b  35283  r1filim  35287  trssfir1om  35295  fineqvnttrclselem3  35307  fineqvinfep  35309  tz9.1regs  35318  trssfir1omregs  35320  gblacfnacd  35324  onvf1odlem1  35325  onvf1odlem4  35328  subgrwlk  35354  erdszelem8  35420  cvmsss2  35496  cvmfolem  35501  fmlasucdisj  35621  satfun  35633  dfon2lem8  36010  dfon2lem9  36011  dfon2  36012  rdgprc  36014  nn0prpwlem  36544  ntruni  36549  clsint2  36551  fneint  36570  fnessref  36579  refssfne  36580  neibastop1  36581  neibastop2lem  36582  bj-0int  37381  bj-ismooredr  37389  relowlpssretop  37646  fvineqsneu  37693  fvineqsneq  37694  heicant  37935  mblfinlem1  37937  ftc2nc  37982  sdclem2  38022  fdc  38025  seqpo  38027  prdsbnd  38073  heibor  38101  rrnequiv  38115  0idl  38305  intidl  38309  unichnidl  38311  prnc  38347  refressn  38813  lsmcv2  39434  lcvexchlem4  39442  lcvexchlem5  39443  eqlkr  39504  paddclN  40247  pclfinN  40305  ldilcnv  40520  ldilco  40521  cdleme25dN  40761  cdlemj2  41227  tendocan  41229  erng1lem  41392  erngdvlem4-rN  41404  dihord2pre  41630  dihglblem2N  41699  dochvalr  41762  hdmap14lem12  42284  hdmap14lem13  42285  supinf  42641  fsuppind  42977  pellfundre  43267  pellfundge  43268  pellfundlb  43270  dford3lem1  43412  aomclem2  43441  oaabsb  43680  cantnf2  43711  ofoafg  43740  naddcnff  43748  naddwordnexlem3  43785  naddwordnexlem4  43787  pwinfi3  43948  iunrelexp0  44087  iunrelexpmin1  44093  iunrelexpmin2  44097  dftrcl3  44105  cnvtrclfv  44109  trclimalb2  44111  dfrtrcl3  44118  ntrneiel2  44471  ntrneik4w  44485  ntrrn  44507  gneispa  44515  gneispb  44516  addrcom  44859  iunconnlem2  45319  ssuzfz  45737  dvnprodlem3  46335  funressnfv  47432  cfsetsnfsetfo  47449  tz6.12-afv  47562  tz6.12-afv2  47629  otiunsndisjX  47668  uniimaprimaeqfv  47771  iccpartltu  47814  iccpartgtl  47815  iccpartleu  47817  iccpartgel  47818  fargshiftf  47829  fargshiftfva  47832  sbgoldbst  48167  bgoldbtbnd  48198  tgblthelfgott  48204  grimuhgr  48276  grimco  48278  isuspgrim0  48283  isuspgrimlem  48284  upgrimpths  48298  gricushgr  48306  grtriclwlk3  48334  stgr0  48349  uspgrlim  48381  grlicsym  48402  nnsgrp  48566  ellcoellss  48824  lindsrng01  48857  suppdm  48899  nn0sumshdiglem1  49010  setrec2fun  50080