Theorem ralrimiv 3120

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralrimiva  3121  ralrimivw  3125  ralrimdv  3127  ralrimivv  3170  rr19.3v  3622  class2seteq  3664  rabssdv  4026  rzalALT  4461  disjord  5081  disjiund  5083  trin  5210  ralxfrALT  5354  otiunsndisj  5463  onmindif  6401  fnprb  7144  fntpb  7145  f1cdmsn  7219  ssorduni  7715  onminex  7738  onmindif2  7743  limuni3  7785  frxp  8059  poxp  8061  sexp2  8079  sexp3  8086  onfununi  8264  onnseq  8267  tfrlem12  8311  tz7.48-2  8364  oaass  8479  omass  8498  oelim2  8513  oelimcl  8518  oaabs2  8567  omabs  8569  uniqs  8701  undifixp  8861  dom2lem  8917  isinf  9154  unblem4  9184  unbnn2  9186  marypha1lem  9323  supssd  9353  supiso  9366  infssd  9384  ordiso2  9407  card2inf  9447  elirrvOLD  9490  wemapwe  9593  ttrclss  9616  trcl  9624  frr3g  9652  tz9.13  9687  rankval3b  9722  rankunb  9746  rankuni2b  9749  scott0  9782  updjud  9830  dfac8alem  9923  carduniima  9990  alephsmo  9996  alephval3  10004  iunfictbso  10008  dfac3  10015  dfac5lem5  10021  dfac12r  10041  dfac12k  10042  kmlem4  10048  kmlem11  10055  cfsuc  10151  cofsmo  10163  cfsmolem  10164  coftr  10167  alephsing  10170  infpssrlem3  10199  fin23lem30  10236  isf32lem2  10248  isf32lem3  10249  isf34lem6  10274  fin1a2lem11  10304  fin1a2lem13  10306  fin1a2s  10308  axcc2lem  10330  domtriomlem  10336  axdc3lem2  10345  axdc4lem  10349  axcclem  10351  axdclem2  10414  iundom2g  10434  uniimadom  10438  cardmin  10458  alephval2  10466  alephreg  10476  fpwwe2lem11  10535  wunex2  10632  wuncval2  10641  tskwe2  10667  inar1  10669  tskuni  10677  gruun  10700  intgru  10708  grutsk1  10715  genpcl  10902  ltexprlem5  10934  suplem1pr  10946  supexpr  10948  supsrlem  11005  axpre-sup  11063  negfi  12074  supaddc  12092  supadd  12093  supmul1  12094  supmullem1  12095  supmul  12097  peano5nni  12131  uzind  12568  zindd  12577  uzwo  12812  lbzbi  12837  xrsupsslem  13209  xrinfmsslem  13210  supxrun  13218  supxrpnf  13220  supxrunb1  13221  supxrunb2  13222  icoshftf1o  13377  flval3  13719  axdc4uzlem  13890  tpfo  14407  wrdnfi  14455  ccatrn  14496  ccatalpha  14500  2cshw  14719  cshweqrep  14727  s3iunsndisj  14875  rtrclreclem4  14968  dfrtrcl2  14969  01sqrexlem1  15149  01sqrexlem6  15154  fsum0diag2  15690  alzdvds  16231  gcdcllem1  16410  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  maxprmfct  16620  hashgcdeq  16701  unbenlem  16820  vdwlem6  16898  vdwlem10  16902  firest  17336  mrieqv2d  17545  iscatd  17579  initoeu2  17923  setcmon  17994  setcepi  17995  fullestrcsetc  18057  fullsetcestrc  18072  isglbd  18415  isacs4lem  18450  acsfiindd  18459  acsmapd  18460  psss  18486  sgrpidmnd  18613  pwmnd  18811  ghmrn  19108  ghmpreima  19117  cntz2ss  19214  symgextres  19304  psgnunilem2  19374  lsmsubg  19533  efgsfo  19618  gsumzaddlem  19800  gsummptnn0fzfv  19866  dmdprdd  19880  dprd2da  19923  ablsimpgprmd  19996  imasring  20215  01eq0ring  20415  isabvd  20697  issrngd  20740  islssd  20838  lbsextlem3  21067  lbsextlem4  21068  lidldvgen  21241  pzriprnglem4  21391  pzriprnglem7  21394  pzriprnglem13  21400  psgnghm  21487  isphld  21561  frlmsslsp  21703  mp2pm2mplem4  22694  tgcl  22854  distop  22880  indistopon  22886  pptbas  22893  toponmre  22978  opnnei  23005  neiuni  23007  neindisj2  23008  ordtrest2  23089  cnpnei  23149  cnindis  23177  cmpcld  23287  uncmp  23288  hauscmplem  23291  2ndc1stc  23336  1stcrest  23338  1stcelcls  23346  llyrest  23370  nllyrest  23371  cldllycmp  23380  reftr  23399  locfincf  23416  comppfsc  23417  txcls  23489  ptpjcn  23496  ptclsg  23500  dfac14lem  23502  xkoccn  23504  txlly  23521  txnlly  23522  ptrescn  23524  tx1stc  23535  xkoco1cn  23542  xkoco2cn  23543  xkococn  23545  xkoinjcn  23572  qtopeu  23601  hmeofval  23643  ordthmeolem  23686  isfild  23743  fbasrn  23769  trfil2  23772  flimclslem  23869  fclsrest  23909  fclscf  23910  flimfcls  23911  alexsubALTlem1  23932  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALT  23936  qustgpopn  24005  isxmetd  24212  imasdsf1olem  24259  blcls  24392  prdsxmslem2  24415  metustfbas  24443  dscmet  24458  nrmmetd  24460  reperflem  24705  reconnlem2  24714  xrge0tsms  24721  fsumcn  24759  cnheibor  24852  tcphcph  25135  lmmbr  25156  caubl  25206  ivthlem1  25350  ovolctb  25389  ovoliunlem2  25402  ovolscalem1  25412  ovolicc2  25421  voliunlem3  25451  ismbfd  25538  mbfimaopnlem  25554  itg2le  25638  ellimc2  25776  c1liplem1  25899  plyeq0lem  26113  dgreq0  26169  aannenlem1  26234  pilem2  26360  cxpcn3lem  26655  scvxcvx  26894  musum  27099  fsumdvdsmul  27103  dchrisum0flb  27419  ostth2lem2  27543  sltval2  27566  nolesgn2ores  27582  nogesgn1ores  27584  nosupres  27617  nosupbnd2lem1  27625  noinfres  27632  noinfbnd2lem1  27640  scutun12  27722  madebdayim  27804  precsexlem9  28124  noseqind  28193  zs12zodd  28363  zs12bday  28365  numedglnl  29093  upgrreslem  29253  umgrreslem  29254  nbuhgr  29292  nbumgr  29296  uhgrnbgr0nb  29303  nbusgrf1o0  29318  uvtxnbgrvtx  29342  cusgrfilem2  29406  uspgr2wlkeq  29595  wwlks  29784  iswwlksnon  29802  rusgr0edg  29922  clwwlkccatlem  29937  clwwisshclwwslem  29962  clwwlkn  29974  clwwlknon  30038  3cyclfrgrrn  30234  vdgn1frgrv3  30245  2wspmdisj  30285  numclwlk2lem2f1o  30327  frgrregord013  30343  htthlem  30865  ocsh  31231  shintcli  31277  pjss2coi  32112  pjnormssi  32116  pjclem4  32147  pj3si  32155  pj3cor1i  32157  strlem3a  32200  strb  32206  hstrlem3a  32208  hstrbi  32214  spansncv2  32241  mdsl1i  32269  cvmdi  32272  mdexchi  32283  h1da  32297  mdsymlem6  32356  sumdmdii  32363  dmdbr5ati  32370  isoun  32652  xrge0tsmsd  33024  ordtrest2NEW  33906  pwsiga  34113  measiun  34201  dya2iocuni  34267  bnj518  34869  bnj1137  34978  bnj1136  34980  bnj1413  35018  bnj1417  35024  bnj60  35045  tz9.1regs  35083  fineqvnttrclselem3  35092  gblacfnacd  35095  onvf1odlem1  35096  onvf1odlem4  35099  subgrwlk  35125  erdszelem8  35191  cvmsss2  35267  cvmfolem  35272  fmlasucdisj  35392  satfun  35404  dfon2lem8  35784  dfon2lem9  35785  dfon2  35786  rdgprc  35788  nn0prpwlem  36316  ntruni  36321  clsint2  36323  fneint  36342  fnessref  36351  refssfne  36352  neibastop1  36353  neibastop2lem  36354  bj-0int  37095  bj-ismooredr  37103  relowlpssretop  37358  fvineqsneu  37405  fvineqsneq  37406  heicant  37655  mblfinlem1  37657  ftc2nc  37702  sdclem2  37742  fdc  37745  seqpo  37747  prdsbnd  37793  heibor  37821  rrnequiv  37835  0idl  38025  intidl  38029  unichnidl  38031  prnc  38067  refressn  38440  lsmcv2  39028  lcvexchlem4  39036  lcvexchlem5  39037  eqlkr  39098  paddclN  39841  pclfinN  39899  ldilcnv  40114  ldilco  40115  cdleme25dN  40355  cdlemj2  40821  tendocan  40823  erng1lem  40986  erngdvlem4-rN  40998  dihord2pre  41224  dihglblem2N  41293  dochvalr  41356  hdmap14lem12  41878  hdmap14lem13  41879  supinf  42235  fsuppind  42583  pellfundre  42874  pellfundge  42875  pellfundlb  42877  dford3lem1  43019  aomclem2  43048  oaabsb  43287  cantnf2  43318  ofoafg  43347  naddcnff  43355  naddwordnexlem3  43392  naddwordnexlem4  43394  pwinfi3  43556  iunrelexp0  43695  iunrelexpmin1  43701  iunrelexpmin2  43705  dftrcl3  43713  cnvtrclfv  43717  trclimalb2  43719  dfrtrcl3  43726  ntrneiel2  44079  ntrneik4w  44093  ntrrn  44115  gneispa  44123  gneispb  44124  addrcom  44468  iunconnlem2  44928  ssuzfz  45349  dvnprodlem3  45949  funressnfv  47047  cfsetsnfsetfo  47064  tz6.12-afv  47177  tz6.12-afv2  47244  otiunsndisjX  47283  uniimaprimaeqfv  47386  iccpartltu  47429  iccpartgtl  47430  iccpartleu  47432  iccpartgel  47433  fargshiftf  47444  fargshiftfva  47447  sbgoldbst  47782  bgoldbtbnd  47813  tgblthelfgott  47819  grimuhgr  47891  grimco  47893  isuspgrim0  47898  isuspgrimlem  47899  upgrimpths  47913  gricushgr  47921  grtriclwlk3  47949  stgr0  47964  uspgrlim  47996  grlicsym  48017  nnsgrp  48181  ellcoellss  48440  lindsrng01  48473  suppdm  48515  nn0sumshdiglem1  48626  setrec2fun  49697