Theorem ralrimiv 3157

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-ral 3081

This theorem is used by:  ralrimiva  3158  ralrimivw  3162  ralrimdv  3164  ralrimivv  3207  rr19.3v  3624  class2seteq  3665  rabssdv  4002  rzalALT  4454  r19.3rzv  4462  disjord  5095  disjiund  5097  trun  5226  trin  5227  ralxfrALT  5381  otiunsndisj  5497  onmindif  6472  fnprb  7234  fntpb  7235  f1cdmsn  7310  ssorduni  7814  onminex  7837  onmindif2  7842  limuni3  7884  ovmptss  8126  frxp  8162  poxp  8164  sexp2  8187  sexp3  8194  onfununi  8374  onnseq  8377  tfrlem12  8422  tz7.48-2  8477  oaass  8594  omass  8613  oelim2  8629  oelimcl  8634  oaabs2  8683  omabs  8685  uniqs  8819  undifixp  8987  dom2lem  9044  isinf  9281  unblem4  9312  unbnn2  9314  marypha1lem  9449  supssd  9479  supiso  9492  infssd  9510  ordiso2  9533  card2inf  9573  elirrvOLDOLD  9617  wemapwe  9722  ttrclss  9745  trcl  9753  frr3g  9784  tz9.13  9822  rankval3b  9860  rankunb  9888  rankuni2b  9891  rankval4b  9904  elhf4  9936  scott0b  9961  scott0OLD  9962  setrec2fun  9997  updjud  10039  dfac8alem  10132  carduniima  10199  alephsmo  10205  alephval3  10213  iunfictbso  10217  dfac3  10224  dfac5lem5  10230  dfac12r  10249  dfac12k  10250  kmlem4  10256  kmlem11  10263  cfsuc  10359  cofsmo  10371  cfsmolem  10372  coftr  10375  alephsing  10378  infpssrlem3  10407  fin23lem30  10444  isf32lem2  10456  isf32lem3  10457  isf34lem6  10482  fin1a2lem11  10512  fin1a2lem13  10514  fin1a2s  10516  axcc2lem  10538  domtriomlem  10544  axdc3lem2  10553  axdc4lem  10557  axcclem  10559  axdclem2  10622  iundom2g  10648  uniimadom  10652  cardmin  10672  alephval2  10681  alephreg  10691  fpwwe2lem11  10750  wunex2  10847  wuncval2  10856  tskwe2  10882  inar1  10884  tskuni  10892  gruun  10915  intgru  10923  grutsk1  10930  genpcl  11117  ltexprlem5  11149  suplem1pr  11161  supexpr  11163  supsrlem  11220  axpre-sup  11278  negfi  12290  supaddc  12308  supadd  12309  supmul1  12310  supmullem1  12311  supmul  12313  peano5nni  12362  uzind  12815  zindd  12824  uzwo  13062  lbzbi  13087  xrsupsslem  13461  xrinfmsslem  13462  supxrun  13470  supxrpnf  13472  supxrunb1  13473  supxrunb2  13474  icoshftf1o  13629  flval3  13979  axdc4uzlem  14150  tpfo  14669  wrdnfi  14717  ccatrn  14759  ccatalpha  14764  2cshw  14989  cshweqrep  14997  s3iunsndisj  15147  rtrclreclem4  15240  dfrtrcl2  15241  01sqrexlem1  15435  01sqrexlem6  15440  fsum0diag2  15975  alzdvds  16516  gcdcllem1  16695  lcmfunsnlem2lem1  16839  lcmfunsnlem2lem2  16840  maxprmfct  16911  hashgcdeq  16993  unbenlem  17112  vdwlem6  17190  vdwlem10  17194  firest  17629  mrieqv2d  17839  iscatd  17873  initoeu2  18217  setcmon  18288  setcepi  18289  fullestrcsetc  18351  fullsetcestrc  18366  isglbd  18709  isacs4lem  18744  acsfiindd  18753  acsmapd  18754  psss  18780  mgmn0plusgf  18853  sgrpidmnd  18954  pwmnd  19169  ghmrn  19469  ghmpreima  19478  cntz2ss  19576  symgextres  19666  psgnunilem2  19736  lsmsubg  19895  efgsfo  19980  gsumzaddlem  20162  gsummptnn0fzfv  20228  dmdprdd  20242  dprd2da  20285  ablsimpgprmd  20358  imasring  20587  01eq0ring  20808  isabvd  21096  issrngd  21139  islssd  21237  lbsextlem3  21465  lbsextlem4  21466  unichnlidl  21543  lidldvgen  21685  pzriprnglem4  21817  pzriprnglem7  21820  pzriprnglem13  21826  psgnghm  21913  isphld  21987  frlmsslsp  22129  mp2pm2mplem4  23154  tgcl  23314  distop  23340  indistopon  23346  pptbas  23353  toponmre  23438  opnnei  23465  neiuni  23467  neindisj2  23468  ordtrest2  23549  cnpnei  23609  cnindis  23637  cmpcld  23747  uncmp  23748  hauscmplem  23751  2ndc1stc  23796  1stcrest  23798  1stcelcls  23807  llyrest  23831  nllyrest  23832  cldllycmp  23841  reftr  23860  locfincf  23877  comppfsc  23878  txcls  23950  ptpjcn  23957  ptclsg  23961  dfac14lem  23963  xkoccn  23965  txlly  23982  txnlly  23983  ptrescn  23985  tx1stc  23996  xkoco1cn  24003  xkoco2cn  24004  xkococn  24006  xkoinjcn  24033  qtopeu  24062  hmeofval  24104  ordthmeolem  24147  isfild  24204  fbasrn  24230  trfil2  24233  flimclslem  24330  fclsrest  24370  fclscf  24371  flimfcls  24372  alexsubALTlem1  24393  alexsubALTlem2  24394  alexsubALTlem3  24395  alexsubALT  24397  qustgpopn  24466  isxmetd  24672  imasdsf1olem  24719  blcls  24852  prdsxmslem2  24875  metustfbas  24903  dscmet  24918  nrmmetd  24920  reperflem  25165  reconnlem2  25174  xrge0tsms  25181  fsumcn  25218  cnheibor  25303  tcphcph  25585  lmmbr  25606  caubl  25656  ivthlem1  25799  ovolctb  25838  ovoliunlem2  25851  ovolscalem1  25861  ovolicc2  25870  voliunlem3  25900  ismbfd  25987  mbfimaopnlem  26003  itg2le  26087  ellimc2  26224  c1liplem1  26343  plyeq0lem  26556  dgreq0  26611  aannenlem1  26682  pilem2  26806  cxpcn3lem  27102  scvxcvx  27340  musum  27545  fsumdvdsmul  27549  dchrisum0flb  27864  ostth2lem2  27988  ltsval2  28040  nolesgn2ores  28056  nogesgn1ores  28058  nosupres  28091  nosupbnd2lem1  28099  noinfres  28106  noinfbnd2lem1  28114  cutsun12  28203  madebdayim  28301  precsexlem9  28628  addonbday  28692  noseqind  28705  z12zsodd  28895  numedglnl  29749  upgrreslem  29912  umgrreslem  29913  nbuhgr  29951  nbumgr  29955  uhgrnbgr0nb  29962  nbusgrf1o0  29977  uvtxnbgrvtx  30001  cusgrfilem2  30064  uspgr2wlkeq  30253  subgrwlk  30296  wwlks  30451  iswwlksnon  30469  rusgr0edg  30592  clwwlkccatlem  30607  clwwisshclwwslem  30632  clwwlkn  30644  clwwlknon  30708  3cyclfrgrrn  30914  vdgn1frgrv3  30925  2wspmdisj  30965  numclwlk2lem2f1o  31007  frgrregord013  31023  htthlem  31546  ocsh  31912  shintcli  31958  pjss2coi  32793  pjnormssi  32797  pjclem4  32828  pj3si  32836  pj3cor1i  32838  strlem3a  32881  strb  32887  hstrlem3a  32889  hstrbi  32895  spansncv2  32922  mdsl1i  32950  cvmdi  32953  mdexchi  32964  h1da  32978  mdsymlem6  33037  sumdmdii  33044  dmdbr5ati  33051  isoun  33363  xrge0tsmsd  33701  ordtrest2NEW  34622  pwsiga  34829  measiun  34918  dya2iocuni  34982  bnj518  35583  bnj1137  35692  bnj1136  35694  bnj1413  35732  bnj1417  35738  bnj60  35759  soinfdom  35797  r1filim  35810  trssfir1om  35818  fineqvnttrclselem3  35890  fineqvinfep  35892  tz9.1regs  35901  trssfir1omregs  35903  gblacfnacd  36028  onvf1odlem1  36030  onvf1odlem4  36033  vonf1oonfo  36048  erdszelem8  36129  cvmsss2  36205  cvmfolem  36210  fmlasucdisj  36330  satfun  36342  mirimanoffr  36626  dfon2lem8  36729  dfon2lem9  36730  dfon2  36731  rdgprc  36733  nn0prpwlem  37287  ntruni  37292  clsint2  37294  fneint  37313  fnessref  37322  refssfne  37323  neibastop1  37324  neibastop2lem  37325  mh-inf3f1  37506  bj-0int  38212  bj-ismooredr  38220  relowlpssretop  38478  fvineqsneu  38525  fvineqsneq  38526  heicant  38764  mblfinlem1  38766  ftc2nc  38811  sdclem2  38867  fdc  38870  seqpo  38872  prdsbnd  38918  heibor  38946  rrnequiv  38960  0idl  39150  intidl  39154  unichnidl  39156  prnc  39192  refressn  39656  lsmcv2  40277  lcvexchlem4  40285  lcvexchlem5  40286  eqlkr  40347  paddclN  41090  pclfinN  41148  ldilcnv  41363  ldilco  41364  cdleme25dN  41604  cdlemj2  42070  tendocan  42072  erng1lem  42235  erngdvlem4-rN  42247  dihord2pre  42473  dihglblem2N  42542  dochvalr  42605  hdmap14lem12  43127  hdmap14lem13  43128  supinf  43484  fsuppind  43809  pellfundre  44079  pellfundge  44080  pellfundlb  44082  dford3lem1  44224  aomclem2  44248  oaabsb  44486  cantnf2  44517  ofoafg  44546  naddcnff  44554  naddwordnexlem3  44591  naddwordnexlem4  44593  pwinfi3  44754  iunrelexp0  44892  iunrelexpmin1  44898  iunrelexpmin2  44902  dftrcl3  44910  cnvtrclfv  44914  trclimalb2  44916  dfrtrcl3  44923  ntrneiel2  45276  ntrneik4w  45290  ntrrn  45312  gneispa  45320  gneispb  45321  addrcom  45646  iunconnlem2  46106  ssuzfz  46564  dvnprodlem3  47161  funressnfv  48316  cfsetsnfsetfo  48333  tz6.12-afv  48446  tz6.12-afv2  48513  otiunsndisjX  48552  uniimaprimaeqfv  48667  iccpartltu  48710  iccpartgtl  48711  iccpartleu  48713  iccpartgel  48714  fargshiftf  48725  fargshiftfva  48728  sbgoldbst  49079  bgoldbtbnd  49110  tgblthelfgott  49116  grimuhgr  49188  grimco  49190  isuspgrim0  49195  isuspgrimlem  49196  upgrimpths  49210  gricushgr  49218  grtriclwlk3  49246  stgr0  49261  uspgrlim  49293  grlicsym  49314  nnsgrp  49477  ellcoellss  49750  lindsrng01  49783  suppdm  49825  nn0sumshdiglem1  49936