Theorem ralrimiv 3181

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-ral 3143

This theorem is referenced by:  ralrimiva  3182  ralrimivw  3183  r19.27vOLD  3185  ralrimdv  3188  ralrimivv  3190  reximdvai  3272  raleleq  3427  rr19.3v  3661  rabssdv  4051  rzal  4453  disjord  5054  disjiund  5056  trin  5182  class2seteq  5255  ralxfrALT  5316  otiunsndisj  5410  onmindif  6280  fnprb  6971  fntpb  6972  ssorduni  7500  onminex  7522  onmindif2  7527  suceloni  7528  limuni3  7567  frxp  7820  poxp  7822  wfrlem15  7969  onfununi  7978  onnseq  7981  tfrlem12  8025  tz7.48-2  8078  oaass  8187  omass  8206  oelim2  8221  oelimcl  8226  oaabs2  8272  omabs  8274  undifixp  8498  dom2lem  8549  isinf  8731  unblem4  8773  unbnn2  8775  marypha1lem  8897  supiso  8939  ordiso2  8979  card2inf  9019  elirrv  9060  wemapwe  9160  trcl  9170  tz9.13  9220  rankval3b  9255  rankunb  9279  rankuni2b  9282  scott0  9315  updjud  9363  dfac8alem  9455  carduniima  9522  alephsmo  9528  alephval3  9536  iunfictbso  9540  dfac3  9547  dfac5lem5  9553  dfac12r  9572  dfac12k  9573  kmlem4  9579  kmlem11  9586  cfsuc  9679  cofsmo  9691  cfsmolem  9692  coftr  9695  alephsing  9698  infpssrlem3  9727  fin23lem30  9764  isf32lem2  9776  isf32lem3  9777  isf34lem6  9802  fin1a2lem11  9832  fin1a2lem13  9834  fin1a2s  9836  axcc2lem  9858  domtriomlem  9864  axdc3lem2  9873  axdc4lem  9877  axcclem  9879  axdclem2  9942  iundom2g  9962  uniimadom  9966  cardmin  9986  alephval2  9994  alephreg  10004  fpwwe2lem12  10063  wunex2  10160  wuncval2  10169  tskwe2  10195  inar1  10197  tskuni  10205  gruun  10228  intgru  10236  grutsk1  10243  genpcl  10430  ltexprlem5  10462  suplem1pr  10474  supexpr  10476  supsrlem  10533  axpre-sup  10591  negfi  11589  fiminreOLD  11590  supaddc  11608  supadd  11609  supmul1  11610  supmullem1  11611  supmul  11613  peano5nni  11641  uzind  12075  zindd  12084  uzwo  12312  lbzbi  12337  xrsupsslem  12701  xrinfmsslem  12702  supxrun  12710  supxrpnf  12712  supxrunb1  12713  supxrunb2  12714  icoshftf1o  12861  flval3  13186  axdc4uzlem  13352  wrdnfi  13899  ccatrn  13943  ccatalpha  13947  2cshw  14175  cshweqrep  14183  s3iunsndisj  14328  rtrclreclem4  14420  dfrtrcl2  14421  sqrlem1  14602  sqrlem6  14607  fsum0diag2  15138  alzdvds  15670  gcdcllem1  15848  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  maxprmfct  16053  hashgcdeq  16126  unbenlem  16244  vdwlem6  16322  vdwlem10  16326  firest  16706  mrieqv2d  16910  iscatd  16944  initoeu2  17276  setcmon  17347  setcepi  17348  fullestrcsetc  17401  fullsetcestrc  17416  isglbd  17727  isacs4lem  17778  acsfiindd  17787  acsmapd  17788  psss  17824  sgrpidmnd  17916  pwmnd  18102  ghmrn  18371  ghmpreima  18380  cntz2ss  18463  symgextres  18553  psgnunilem2  18623  lsmsubg  18779  efgsfo  18865  gsumzaddlem  19041  gsummptnn0fzfv  19107  dmdprdd  19121  dprd2da  19164  ablsimpgprmd  19237  imasring  19369  isabvd  19591  issrngd  19632  islssd  19707  lbsextlem3  19932  lbsextlem4  19933  lidldvgen  20028  psgnghm  20724  isphld  20798  frlmsslsp  20940  mp2pm2mplem4  21417  tgcl  21577  distop  21603  indistopon  21609  pptbas  21616  toponmre  21701  opnnei  21728  neiuni  21730  neindisj2  21731  ordtrest2  21812  cnpnei  21872  cnindis  21900  cmpcld  22010  uncmp  22011  hauscmplem  22014  2ndc1stc  22059  1stcrest  22061  1stcelcls  22069  llyrest  22093  nllyrest  22094  cldllycmp  22103  reftr  22122  locfincf  22139  comppfsc  22140  txcls  22212  ptpjcn  22219  ptclsg  22223  dfac14lem  22225  xkoccn  22227  txlly  22244  txnlly  22245  ptrescn  22247  tx1stc  22258  xkoco1cn  22265  xkoco2cn  22266  xkococn  22268  xkoinjcn  22295  qtopeu  22324  hmeofval  22366  ordthmeolem  22409  isfild  22466  fbasrn  22492  trfil2  22495  flimclslem  22592  fclsrest  22632  fclscf  22633  flimfcls  22634  alexsubALTlem1  22655  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALT  22659  qustgpopn  22728  isxmetd  22936  imasdsf1olem  22983  blcls  23116  prdsxmslem2  23139  metustfbas  23167  dscmet  23182  nrmmetd  23184  reperflem  23426  reconnlem2  23435  xrge0tsms  23442  fsumcn  23478  cnheibor  23559  tcphcph  23840  lmmbr  23861  caubl  23911  ivthlem1  24052  ovolctb  24091  ovoliunlem2  24104  ovolscalem1  24114  ovolicc2  24123  voliunlem3  24153  ismbfd  24240  mbfimaopnlem  24256  itg2le  24340  ellimc2  24475  c1liplem1  24593  plyeq0lem  24800  dgreq0  24855  aannenlem1  24917  pilem2  25040  cxpcn3lem  25328  scvxcvx  25563  musum  25768  dchrisum0flb  26086  ostth2lem2  26210  numedglnl  26929  upgrreslem  27086  umgrreslem  27087  nbuhgr  27125  nbumgr  27129  uhgrnbgr0nb  27136  nbusgrf1o0  27151  uvtxnbgrvtx  27175  cusgrfilem2  27238  uspgr2wlkeq  27427  wwlks  27613  iswwlksnon  27631  rusgr0edg  27752  clwwlkccatlem  27767  clwwisshclwwslem  27792  clwwlkn  27804  clwwlknon  27869  3cyclfrgrrn  28065  vdgn1frgrv3  28076  2wspmdisj  28116  numclwlk2lem2f1o  28158  frgrregord013  28174  htthlem  28694  ocsh  29060  shintcli  29106  pjss2coi  29941  pjnormssi  29945  pjclem4  29976  pj3si  29984  pj3cor1i  29986  strlem3a  30029  strb  30035  hstrlem3a  30037  hstrbi  30043  spansncv2  30070  mdsl1i  30098  cvmdi  30101  mdexchi  30112  h1da  30126  mdsymlem6  30185  sumdmdii  30192  dmdbr5ati  30199  isoun  30437  supssd  30445  infssd  30446  xrge0tsmsd  30692  ordtrest2NEW  31166  pwsiga  31389  measiun  31477  dya2iocuni  31541  bnj518  32158  bnj1137  32267  bnj1136  32269  bnj1413  32307  bnj1417  32313  bnj60  32334  subgrwlk  32379  erdszelem8  32445  cvmsss2  32521  cvmfolem  32526  fmlasucdisj  32646  satfun  32658  dfon2lem8  33035  dfon2lem9  33036  dfon2  33037  rdgprc  33039  trpredtr  33069  trpredmintr  33070  trpredelss  33071  dftrpred3g  33072  trpredpo  33074  trpredrec  33077  frr3g  33121  sltval2  33163  nolesgn2ores  33179  nosupres  33207  nosupbnd2lem1  33215  scutun12  33271  nn0prpwlem  33670  ntruni  33675  clsint2  33677  fneint  33696  fnessref  33705  refssfne  33706  neibastop1  33707  neibastop2lem  33708  bj-0int  34396  bj-ismooredr  34404  relowlpssretop  34648  fvineqsneu  34695  fvineqsneq  34696  heicant  34942  mblfinlem1  34944  ftc2nc  34991  sdclem2  35032  fdc  35035  seqpo  35037  prdsbnd  35086  heibor  35114  rrnequiv  35128  0idl  35318  intidl  35322  unichnidl  35324  prnc  35360  uniqsALTV  35601  lsmcv2  36180  lcvexchlem4  36188  lcvexchlem5  36189  eqlkr  36250  paddclN  36993  pclfinN  37051  ldilcnv  37266  ldilco  37267  cdleme25dN  37507  cdlemj2  37973  tendocan  37975  erng1lem  38138  erngdvlem4-rN  38150  dihord2pre  38376  dihglblem2N  38445  dochvalr  38508  hdmap14lem12  39030  hdmap14lem13  39031  pellfundre  39498  pellfundge  39499  pellfundlb  39501  dford3lem1  39643  aomclem2  39675  pwinfi3  39942  iunrelexp0  40067  iunrelexpmin1  40073  iunrelexpmin2  40077  dftrcl3  40085  cnvtrclfv  40089  trclimalb2  40091  dfrtrcl3  40098  ntrneiel2  40456  ntrneik4w  40470  ntrrn  40492  gneispa  40500  gneispb  40501  addrcom  40827  iunconnlem2  41289  ssuzfz  41637  dvmptfprod  42250  dvnprodlem3  42253  funressnfv  43298  tz6.12-afv  43392  tz6.12-afv2  43459  otiunsndisjX  43498  uniimaprimaeqfv  43562  iccpartltu  43605  iccpartgtl  43606  iccpartleu  43608  iccpartgel  43609  fargshiftf  43620  fargshiftfva  43623  sbgoldbst  43963  bgoldbtbnd  43994  tgblthelfgott  44000  isomushgr  44011  nnsgrp  44104  ellcoellss  44510  lindsrng01  44543  suppdm  44585  nn0sumshdiglem1  44701  setrec2fun  44815