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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

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  3428  rr19.3v  3661  rabssdv  4051  rzal  4453  disjord  5047  disjiund  5049  trin  5175  class2seteq  5248  ralxfrALT  5308  otiunsndisj  5403  onmindif  6275  fnprb  6965  fntpb  6966  ssorduni  7494  onminex  7516  onmindif2  7521  suceloni  7522  limuni3  7561  frxp  7814  poxp  7816  wfrlem15  7963  onfununi  7972  onnseq  7975  tfrlem12  8019  tz7.48-2  8072  oaass  8181  omass  8200  oelim2  8215  oelimcl  8220  oaabs2  8266  omabs  8268  undifixp  8492  dom2lem  8543  isinf  8725  unblem4  8767  unbnn2  8769  marypha1lem  8891  supiso  8933  ordiso2  8973  card2inf  9013  elirrv  9054  wemapwe  9154  trcl  9164  tz9.13  9214  rankval3b  9249  rankunb  9273  rankuni2b  9276  scott0  9309  updjud  9357  dfac8alem  9449  carduniima  9516  alephsmo  9522  alephval3  9530  iunfictbso  9534  dfac3  9541  dfac5lem5  9547  dfac12r  9566  dfac12k  9567  kmlem4  9573  kmlem11  9580  cfsuc  9673  cofsmo  9685  cfsmolem  9686  coftr  9689  alephsing  9692  infpssrlem3  9721  fin23lem30  9758  isf32lem2  9770  isf32lem3  9771  isf34lem6  9796  fin1a2lem11  9826  fin1a2lem13  9828  fin1a2s  9830  axcc2lem  9852  domtriomlem  9858  axdc3lem2  9867  axdc4lem  9871  axcclem  9873  axdclem2  9936  iundom2g  9956  uniimadom  9960  cardmin  9980  alephval2  9988  alephreg  9998  fpwwe2lem12  10057  wunex2  10154  wuncval2  10163  tskwe2  10189  inar1  10191  tskuni  10199  gruun  10222  intgru  10230  grutsk1  10237  genpcl  10424  ltexprlem5  10456  suplem1pr  10468  supexpr  10470  supsrlem  10527  axpre-sup  10585  negfi  11583  fiminreOLD  11584  supaddc  11602  supadd  11603  supmul1  11604  supmullem1  11605  supmul  11607  peano5nni  11635  uzind  12068  zindd  12077  uzwo  12305  lbzbi  12330  xrsupsslem  12694  xrinfmsslem  12695  supxrun  12703  supxrpnf  12705  supxrunb1  12706  supxrunb2  12707  icoshftf1o  12854  flval3  13179  axdc4uzlem  13345  wrdnfi  13893  ccatrn  13937  ccatalpha  13941  2cshw  14169  cshweqrep  14177  s3iunsndisj  14322  rtrclreclem4  14414  dfrtrcl2  14415  sqrlem1  14596  sqrlem6  14601  fsum0diag2  15132  alzdvds  15664  gcdcllem1  15842  lcmfunsnlem2lem1  15976  lcmfunsnlem2lem2  15977  maxprmfct  16047  hashgcdeq  16120  unbenlem  16238  vdwlem6  16316  vdwlem10  16320  firest  16700  mrieqv2d  16904  iscatd  16938  initoeu2  17270  setcmon  17341  setcepi  17342  fullestrcsetc  17395  fullsetcestrc  17410  isglbd  17721  isacs4lem  17772  acsfiindd  17781  acsmapd  17782  psss  17818  sgrpidmnd  17910  pwmnd  18096  ghmrn  18365  ghmpreima  18374  cntz2ss  18457  symgextres  18547  psgnunilem2  18617  lsmsubg  18773  efgsfo  18859  gsumzaddlem  19035  gsummptnn0fzfv  19101  dmdprdd  19115  dprd2da  19158  ablsimpgprmd  19231  imasring  19363  isabvd  19585  issrngd  19626  islssd  19701  lbsextlem3  19926  lbsextlem4  19927  lidldvgen  20022  psgnghm  20718  isphld  20792  frlmsslsp  20934  mp2pm2mplem4  21411  tgcl  21571  distop  21597  indistopon  21603  pptbas  21610  toponmre  21695  opnnei  21722  neiuni  21724  neindisj2  21725  ordtrest2  21806  cnpnei  21866  cnindis  21894  cmpcld  22004  uncmp  22005  hauscmplem  22008  2ndc1stc  22053  1stcrest  22055  1stcelcls  22063  llyrest  22087  nllyrest  22088  cldllycmp  22097  reftr  22116  locfincf  22133  comppfsc  22134  txcls  22206  ptpjcn  22213  ptclsg  22217  dfac14lem  22219  xkoccn  22221  txlly  22238  txnlly  22239  ptrescn  22241  tx1stc  22252  xkoco1cn  22259  xkoco2cn  22260  xkococn  22262  xkoinjcn  22289  qtopeu  22318  hmeofval  22360  ordthmeolem  22403  isfild  22460  fbasrn  22486  trfil2  22489  flimclslem  22586  fclsrest  22626  fclscf  22627  flimfcls  22628  alexsubALTlem1  22649  alexsubALTlem2  22650  alexsubALTlem3  22651  alexsubALT  22653  qustgpopn  22722  isxmetd  22930  imasdsf1olem  22977  blcls  23110  prdsxmslem2  23133  metustfbas  23161  dscmet  23176  nrmmetd  23178  reperflem  23420  reconnlem2  23429  xrge0tsms  23436  fsumcn  23472  cnheibor  23553  tcphcph  23834  lmmbr  23855  caubl  23905  ivthlem1  24046  ovolctb  24085  ovoliunlem2  24098  ovolscalem1  24108  ovolicc2  24117  voliunlem3  24147  ismbfd  24234  mbfimaopnlem  24250  itg2le  24334  ellimc2  24469  c1liplem1  24587  plyeq0lem  24794  dgreq0  24849  aannenlem1  24911  pilem2  25034  cxpcn3lem  25322  scvxcvx  25557  musum  25762  dchrisum0flb  26080  ostth2lem2  26204  numedglnl  26923  upgrreslem  27080  umgrreslem  27081  nbuhgr  27119  nbumgr  27123  uhgrnbgr0nb  27130  nbusgrf1o0  27145  uvtxnbgrvtx  27169  cusgrfilem2  27232  uspgr2wlkeq  27421  wwlks  27607  iswwlksnon  27625  rusgr0edg  27746  clwwlkccatlem  27761  clwwisshclwwslem  27786  clwwlkn  27798  clwwlknon  27863  3cyclfrgrrn  28059  vdgn1frgrv3  28070  2wspmdisj  28110  numclwlk2lem2f1o  28152  frgrregord013  28168  htthlem  28688  ocsh  29054  shintcli  29100  pjss2coi  29935  pjnormssi  29939  pjclem4  29970  pj3si  29978  pj3cor1i  29980  strlem3a  30023  strb  30029  hstrlem3a  30031  hstrbi  30037  spansncv2  30064  mdsl1i  30092  cvmdi  30095  mdexchi  30106  h1da  30120  mdsymlem6  30179  sumdmdii  30186  dmdbr5ati  30193  isoun  30431  supssd  30439  infssd  30440  xrge0tsmsd  30687  ordtrest2NEW  31161  pwsiga  31384  measiun  31472  dya2iocuni  31536  bnj518  32153  bnj1137  32262  bnj1136  32264  bnj1413  32302  bnj1417  32308  bnj60  32329  subgrwlk  32374  erdszelem8  32440  cvmsss2  32516  cvmfolem  32521  fmlasucdisj  32641  satfun  32653  dfon2lem8  33030  dfon2lem9  33031  dfon2  33032  rdgprc  33034  trpredtr  33064  trpredmintr  33065  trpredelss  33066  dftrpred3g  33067  trpredpo  33069  trpredrec  33072  frr3g  33116  sltval2  33158  nolesgn2ores  33174  nosupres  33202  nosupbnd2lem1  33210  scutun12  33266  nn0prpwlem  33665  ntruni  33670  clsint2  33672  fneint  33691  fnessref  33700  refssfne  33701  neibastop1  33702  neibastop2lem  33703  bj-0int  34387  bj-ismooredr  34395  relowlpssretop  34639  fvineqsneu  34686  fvineqsneq  34687  heicant  34921  mblfinlem1  34923  ftc2nc  34970  sdclem2  35011  fdc  35014  seqpo  35016  prdsbnd  35065  heibor  35093  rrnequiv  35107  0idl  35297  intidl  35301  unichnidl  35303  prnc  35339  uniqsALTV  35580  lsmcv2  36159  lcvexchlem4  36167  lcvexchlem5  36168  eqlkr  36229  paddclN  36972  pclfinN  37030  ldilcnv  37245  ldilco  37246  cdleme25dN  37486  cdlemj2  37952  tendocan  37954  erng1lem  38117  erngdvlem4-rN  38129  dihord2pre  38355  dihglblem2N  38424  dochvalr  38487  hdmap14lem12  39009  hdmap14lem13  39010  pellfundre  39471  pellfundge  39472  pellfundlb  39474  dford3lem1  39616  aomclem2  39648  pwinfi3  39915  iunrelexp0  40040  iunrelexpmin1  40046  iunrelexpmin2  40050  dftrcl3  40058  cnvtrclfv  40062  trclimalb2  40064  dfrtrcl3  40071  ntrneiel2  40429  ntrneik4w  40443  ntrrn  40465  gneispa  40473  gneispb  40474  addrcom  40800  iunconnlem2  41262  ssuzfz  41609  dvmptfprod  42222  dvnprodlem3  42225  funressnfv  43271  tz6.12-afv  43365  tz6.12-afv2  43432  otiunsndisjX  43471  uniimaprimaeqfv  43535  iccpartltu  43578  iccpartgtl  43579  iccpartleu  43581  iccpartgel  43582  fargshiftf  43593  fargshiftfva  43596  sbgoldbst  43936  bgoldbtbnd  43967  tgblthelfgott  43973  isomushgr  43984  nnsgrp  44077  ellcoellss  44483  lindsrng01  44516  suppdm  44558  nn0sumshdiglem1  44674  setrec2fun  44788