Theorem ralrimiv 3102

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ral 3069

This theorem is referenced by:  ralrimiva  3103  ralrimivw  3104  ralrimdv  3105  ralrimivv  3122  reximdvaiOLD  3201  raleleq  3356  rr19.3v  3598  rabssdv  4008  rzalALT  4440  disjord  5062  disjiund  5064  trin  5201  class2seteq  5277  ralxfrALT  5338  otiunsndisj  5434  onmindif  6355  fnprb  7084  fntpb  7085  f1cdmsn  7154  ssorduni  7629  onminex  7652  onmindif2  7657  sucexeloni  7658  suceloniOLD  7660  limuni3  7699  frxp  7967  poxp  7969  wfrlem15OLD  8154  onfununi  8172  onnseq  8175  tfrlem12  8220  tz7.48-2  8273  oaass  8392  omass  8411  oelim2  8426  oelimcl  8431  oaabs2  8479  omabs  8481  undifixp  8722  dom2lem  8780  isinf  9036  unblem4  9069  unbnn2  9071  marypha1lem  9192  supiso  9234  ordiso2  9274  card2inf  9314  elirrv  9355  wemapwe  9455  ttrclss  9478  trcl  9486  frr3g  9514  tz9.13  9549  rankval3b  9584  rankunb  9608  rankuni2b  9611  scott0  9644  updjud  9692  dfac8alem  9785  carduniima  9852  alephsmo  9858  alephval3  9866  iunfictbso  9870  dfac3  9877  dfac5lem5  9883  dfac12r  9902  dfac12k  9903  kmlem4  9909  kmlem11  9916  cfsuc  10013  cofsmo  10025  cfsmolem  10026  coftr  10029  alephsing  10032  infpssrlem3  10061  fin23lem30  10098  isf32lem2  10110  isf32lem3  10111  isf34lem6  10136  fin1a2lem11  10166  fin1a2lem13  10168  fin1a2s  10170  axcc2lem  10192  domtriomlem  10198  axdc3lem2  10207  axdc4lem  10211  axcclem  10213  axdclem2  10276  iundom2g  10296  uniimadom  10300  cardmin  10320  alephval2  10328  alephreg  10338  fpwwe2lem11  10397  wunex2  10494  wuncval2  10503  tskwe2  10529  inar1  10531  tskuni  10539  gruun  10562  intgru  10570  grutsk1  10577  genpcl  10764  ltexprlem5  10796  suplem1pr  10808  supexpr  10810  supsrlem  10867  axpre-sup  10925  negfi  11924  supaddc  11942  supadd  11943  supmul1  11944  supmullem1  11945  supmul  11947  peano5nni  11976  uzind  12412  zindd  12421  uzwo  12651  lbzbi  12676  xrsupsslem  13041  xrinfmsslem  13042  supxrun  13050  supxrpnf  13052  supxrunb1  13053  supxrunb2  13054  icoshftf1o  13206  flval3  13535  axdc4uzlem  13703  wrdnfi  14251  ccatrn  14294  ccatalpha  14298  2cshw  14526  cshweqrep  14534  s3iunsndisj  14679  rtrclreclem4  14772  dfrtrcl2  14773  sqrlem1  14954  sqrlem6  14959  fsum0diag2  15495  alzdvds  16029  gcdcllem1  16206  lcmfunsnlem2lem1  16343  lcmfunsnlem2lem2  16344  maxprmfct  16414  hashgcdeq  16490  unbenlem  16609  vdwlem6  16687  vdwlem10  16691  firest  17143  mrieqv2d  17348  iscatd  17382  initoeu2  17731  setcmon  17802  setcepi  17803  fullestrcsetc  17868  fullsetcestrc  17883  isglbd  18227  isacs4lem  18262  acsfiindd  18271  acsmapd  18272  psss  18298  sgrpidmnd  18390  pwmnd  18576  ghmrn  18847  ghmpreima  18856  cntz2ss  18939  symgextres  19033  psgnunilem2  19103  lsmsubg  19259  efgsfo  19345  gsumzaddlem  19522  gsummptnn0fzfv  19588  dmdprdd  19602  dprd2da  19645  ablsimpgprmd  19718  imasring  19858  isabvd  20080  issrngd  20121  islssd  20197  lbsextlem3  20422  lbsextlem4  20423  lidldvgen  20526  psgnghm  20785  isphld  20859  frlmsslsp  21003  mp2pm2mplem4  21958  tgcl  22119  distop  22145  indistopon  22151  pptbas  22158  toponmre  22244  opnnei  22271  neiuni  22273  neindisj2  22274  ordtrest2  22355  cnpnei  22415  cnindis  22443  cmpcld  22553  uncmp  22554  hauscmplem  22557  2ndc1stc  22602  1stcrest  22604  1stcelcls  22612  llyrest  22636  nllyrest  22637  cldllycmp  22646  reftr  22665  locfincf  22682  comppfsc  22683  txcls  22755  ptpjcn  22762  ptclsg  22766  dfac14lem  22768  xkoccn  22770  txlly  22787  txnlly  22788  ptrescn  22790  tx1stc  22801  xkoco1cn  22808  xkoco2cn  22809  xkococn  22811  xkoinjcn  22838  qtopeu  22867  hmeofval  22909  ordthmeolem  22952  isfild  23009  fbasrn  23035  trfil2  23038  flimclslem  23135  fclsrest  23175  fclscf  23176  flimfcls  23177  alexsubALTlem1  23198  alexsubALTlem2  23199  alexsubALTlem3  23200  alexsubALT  23202  qustgpopn  23271  isxmetd  23479  imasdsf1olem  23526  blcls  23662  prdsxmslem2  23685  metustfbas  23713  dscmet  23728  nrmmetd  23730  reperflem  23981  reconnlem2  23990  xrge0tsms  23997  fsumcn  24033  cnheibor  24118  tcphcph  24401  lmmbr  24422  caubl  24472  ivthlem1  24615  ovolctb  24654  ovoliunlem2  24667  ovolscalem1  24677  ovolicc2  24686  voliunlem3  24716  ismbfd  24803  mbfimaopnlem  24819  itg2le  24904  ellimc2  25041  c1liplem1  25160  plyeq0lem  25371  dgreq0  25426  aannenlem1  25488  pilem2  25611  cxpcn3lem  25900  scvxcvx  26135  musum  26340  dchrisum0flb  26658  ostth2lem2  26782  numedglnl  27514  upgrreslem  27671  umgrreslem  27672  nbuhgr  27710  nbumgr  27714  uhgrnbgr0nb  27721  nbusgrf1o0  27736  uvtxnbgrvtx  27760  cusgrfilem2  27823  uspgr2wlkeq  28013  wwlks  28200  iswwlksnon  28218  rusgr0edg  28338  clwwlkccatlem  28353  clwwisshclwwslem  28378  clwwlkn  28390  clwwlknon  28454  3cyclfrgrrn  28650  vdgn1frgrv3  28661  2wspmdisj  28701  numclwlk2lem2f1o  28743  frgrregord013  28759  htthlem  29279  ocsh  29645  shintcli  29691  pjss2coi  30526  pjnormssi  30530  pjclem4  30561  pj3si  30569  pj3cor1i  30571  strlem3a  30614  strb  30620  hstrlem3a  30622  hstrbi  30628  spansncv2  30655  mdsl1i  30683  cvmdi  30686  mdexchi  30697  h1da  30711  mdsymlem6  30770  sumdmdii  30777  dmdbr5ati  30784  isoun  31034  supssd  31044  infssd  31045  xrge0tsmsd  31317  ordtrest2NEW  31873  pwsiga  32098  measiun  32186  dya2iocuni  32250  bnj518  32866  bnj1137  32975  bnj1136  32977  bnj1413  33015  bnj1417  33021  bnj60  33042  subgrwlk  33094  erdszelem8  33160  cvmsss2  33236  cvmfolem  33241  fmlasucdisj  33361  satfun  33373  dfon2lem8  33766  dfon2lem9  33767  dfon2  33768  rdgprc  33770  sexp2  33793  sexp3  33799  sltval2  33859  nolesgn2ores  33875  nogesgn1ores  33877  nosupres  33910  nosupbnd2lem1  33918  noinfres  33925  noinfbnd2lem1  33933  scutun12  34004  madebdayim  34070  nn0prpwlem  34511  ntruni  34516  clsint2  34518  fneint  34537  fnessref  34546  refssfne  34547  neibastop1  34548  neibastop2lem  34549  bj-0int  35272  bj-ismooredr  35280  relowlpssretop  35535  fvineqsneu  35582  fvineqsneq  35583  heicant  35812  mblfinlem1  35814  ftc2nc  35859  sdclem2  35900  fdc  35903  seqpo  35905  prdsbnd  35951  heibor  35979  rrnequiv  35993  0idl  36183  intidl  36187  unichnidl  36189  prnc  36225  uniqsALTV  36464  lsmcv2  37043  lcvexchlem4  37051  lcvexchlem5  37052  eqlkr  37113  paddclN  37856  pclfinN  37914  ldilcnv  38129  ldilco  38130  cdleme25dN  38370  cdlemj2  38836  tendocan  38838  erng1lem  39001  erngdvlem4-rN  39013  dihord2pre  39239  dihglblem2N  39308  dochvalr  39371  hdmap14lem12  39893  hdmap14lem13  39894  fsuppind  40279  pellfundre  40703  pellfundge  40704  pellfundlb  40706  dford3lem1  40848  aomclem2  40880  pwinfi3  41170  iunrelexp0  41310  iunrelexpmin1  41316  iunrelexpmin2  41320  dftrcl3  41328  cnvtrclfv  41332  trclimalb2  41334  dfrtrcl3  41341  ntrneiel2  41696  ntrneik4w  41710  ntrrn  41732  gneispa  41740  gneispb  41741  addrcom  42093  iunconnlem2  42555  ssuzfz  42888  dvmptfprod  43486  dvnprodlem3  43489  funressnfv  44537  cfsetsnfsetfo  44554  tz6.12-afv  44665  tz6.12-afv2  44732  otiunsndisjX  44771  uniimaprimaeqfv  44834  iccpartltu  44877  iccpartgtl  44878  iccpartleu  44880  iccpartgel  44881  fargshiftf  44892  fargshiftfva  44895  sbgoldbst  45230  bgoldbtbnd  45261  tgblthelfgott  45267  isomushgr  45278  nnsgrp  45371  ellcoellss  45776  lindsrng01  45809  suppdm  45851  nn0sumshdiglem1  45967  setrec2fun  46398