Theorem ralrimiv 3153

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  ralrimiva  3154  ralrimivw  3158  ralrimdv  3160  ralrimivv  3203  rr19.3v  3620  class2seteq  3661  rabssdv  3999  rzalALT  4450  r19.3rzv  4458  disjord  5091  disjiund  5093  trun  5222  trin  5223  ralxfrALT  5376  otiunsndisj  5492  onmindif  6457  fnprb  7214  fntpb  7215  f1cdmsn  7290  ssorduni  7793  onminex  7816  onmindif2  7821  limuni3  7863  frxp  8138  poxp  8140  sexp2  8163  sexp3  8170  onfununi  8349  onnseq  8352  tfrlem12  8397  tz7.48-2  8452  oaass  8569  omass  8588  oelim2  8604  oelimcl  8609  oaabs2  8658  omabs  8660  uniqs  8794  undifixp  8962  dom2lem  9019  isinf  9256  unblem4  9287  unbnn2  9289  marypha1lem  9425  supssd  9455  supiso  9468  infssd  9486  ordiso2  9509  card2inf  9549  elirrvOLDOLD  9593  wemapwe  9698  ttrclss  9721  trcl  9729  frr3g  9760  tz9.13  9798  rankval3b  9836  rankunb  9864  rankuni2b  9867  rankval4b  9880  elhf4  9912  scott0b  9937  scott0OLD  9938  setrec2fun  9973  updjud  10015  dfac8alem  10108  carduniima  10175  alephsmo  10181  alephval3  10189  iunfictbso  10193  dfac3  10200  dfac5lem5  10206  dfac12r  10225  dfac12k  10226  kmlem4  10232  kmlem11  10239  cfsuc  10335  cofsmo  10347  cfsmolem  10348  coftr  10351  alephsing  10354  infpssrlem3  10383  fin23lem30  10420  isf32lem2  10432  isf32lem3  10433  isf34lem6  10458  fin1a2lem11  10488  fin1a2lem13  10490  fin1a2s  10492  axcc2lem  10514  domtriomlem  10520  axdc3lem2  10529  axdc4lem  10533  axcclem  10535  axdclem2  10598  iundom2g  10624  uniimadom  10628  cardmin  10648  alephval2  10657  alephreg  10667  fpwwe2lem11  10726  wunex2  10823  wuncval2  10832  tskwe2  10858  inar1  10860  tskuni  10868  gruun  10891  intgru  10899  grutsk1  10906  genpcl  11093  ltexprlem5  11125  suplem1pr  11137  supexpr  11139  supsrlem  11196  axpre-sup  11254  negfi  12266  supaddc  12284  supadd  12285  supmul1  12286  supmullem1  12287  supmul  12289  peano5nni  12338  uzind  12791  zindd  12800  uzwo  13038  lbzbi  13063  xrsupsslem  13437  xrinfmsslem  13438  supxrun  13446  supxrpnf  13448  supxrunb1  13449  supxrunb2  13450  icoshftf1o  13605  flval3  13955  axdc4uzlem  14126  tpfo  14645  wrdnfi  14693  ccatrn  14735  ccatalpha  14740  2cshw  14964  cshweqrep  14972  s3iunsndisj  15121  rtrclreclem4  15214  dfrtrcl2  15215  01sqrexlem1  15409  01sqrexlem6  15414  fsum0diag2  15949  alzdvds  16490  gcdcllem1  16669  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  maxprmfct  16885  hashgcdeq  16967  unbenlem  17086  vdwlem6  17164  vdwlem10  17168  firest  17603  mrieqv2d  17813  iscatd  17847  initoeu2  18191  setcmon  18262  setcepi  18263  fullestrcsetc  18325  fullsetcestrc  18340  isglbd  18683  isacs4lem  18718  acsfiindd  18727  acsmapd  18728  psss  18754  mgmn0plusgf  18827  sgrpidmnd  18928  pwmnd  19143  ghmrn  19443  ghmpreima  19452  cntz2ss  19549  symgextres  19639  psgnunilem2  19709  lsmsubg  19868  efgsfo  19953  gsumzaddlem  20135  gsummptnn0fzfv  20201  dmdprdd  20215  dprd2da  20258  ablsimpgprmd  20331  imasring  20560  01eq0ring  20781  isabvd  21069  issrngd  21112  islssd  21210  lbsextlem3  21438  lbsextlem4  21439  unichnlidl  21516  lidldvgen  21658  pzriprnglem4  21790  pzriprnglem7  21793  pzriprnglem13  21799  psgnghm  21886  isphld  21960  frlmsslsp  22102  mp2pm2mplem4  23127  tgcl  23287  distop  23313  indistopon  23319  pptbas  23326  toponmre  23411  opnnei  23438  neiuni  23440  neindisj2  23441  ordtrest2  23522  cnpnei  23582  cnindis  23610  cmpcld  23720  uncmp  23721  hauscmplem  23724  2ndc1stc  23769  1stcrest  23771  1stcelcls  23780  llyrest  23804  nllyrest  23805  cldllycmp  23814  reftr  23833  locfincf  23850  comppfsc  23851  txcls  23923  ptpjcn  23930  ptclsg  23934  dfac14lem  23936  xkoccn  23938  txlly  23955  txnlly  23956  ptrescn  23958  tx1stc  23969  xkoco1cn  23976  xkoco2cn  23977  xkococn  23979  xkoinjcn  24006  qtopeu  24035  hmeofval  24077  ordthmeolem  24120  isfild  24177  fbasrn  24203  trfil2  24206  flimclslem  24303  fclsrest  24343  fclscf  24344  flimfcls  24345  alexsubALTlem1  24366  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALT  24370  qustgpopn  24439  isxmetd  24645  imasdsf1olem  24692  blcls  24825  prdsxmslem2  24848  metustfbas  24876  dscmet  24891  nrmmetd  24893  reperflem  25138  reconnlem2  25147  xrge0tsms  25154  fsumcn  25191  cnheibor  25276  tcphcph  25558  lmmbr  25579  caubl  25629  ivthlem1  25772  ovolctb  25811  ovoliunlem2  25824  ovolscalem1  25834  ovolicc2  25843  voliunlem3  25873  ismbfd  25960  mbfimaopnlem  25976  itg2le  26060  ellimc2  26197  c1liplem1  26316  plyeq0lem  26529  dgreq0  26584  aannenlem1  26655  pilem2  26779  cxpcn3lem  27075  scvxcvx  27313  musum  27518  fsumdvdsmul  27522  dchrisum0flb  27837  ostth2lem2  27961  ltsval2  28013  nolesgn2ores  28029  nogesgn1ores  28031  nosupres  28064  nosupbnd2lem1  28072  noinfres  28079  noinfbnd2lem1  28087  cutsun12  28176  madebdayim  28274  precsexlem9  28601  addonbday  28665  noseqind  28678  z12zsodd  28868  numedglnl  29722  upgrreslem  29885  umgrreslem  29886  nbuhgr  29924  nbumgr  29928  uhgrnbgr0nb  29935  nbusgrf1o0  29950  uvtxnbgrvtx  29974  cusgrfilem2  30037  uspgr2wlkeq  30226  subgrwlk  30269  wwlks  30424  iswwlksnon  30442  rusgr0edg  30565  clwwlkccatlem  30580  clwwisshclwwslem  30605  clwwlkn  30617  clwwlknon  30681  3cyclfrgrrn  30887  vdgn1frgrv3  30898  2wspmdisj  30938  numclwlk2lem2f1o  30980  frgrregord013  30996  htthlem  31519  ocsh  31885  shintcli  31931  pjss2coi  32766  pjnormssi  32770  pjclem4  32801  pj3si  32809  pj3cor1i  32811  strlem3a  32854  strb  32860  hstrlem3a  32862  hstrbi  32868  spansncv2  32895  mdsl1i  32923  cvmdi  32926  mdexchi  32937  h1da  32951  mdsymlem6  33010  sumdmdii  33017  dmdbr5ati  33024  isoun  33295  xrge0tsmsd  33634  ordtrest2NEW  34555  pwsiga  34762  measiun  34851  dya2iocuni  34915  bnj518  35516  bnj1137  35625  bnj1136  35627  bnj1413  35665  bnj1417  35671  bnj60  35692  soinfdom  35717  r1filim  35729  trssfir1om  35737  fineqvnttrclselem3  35791  fineqvinfep  35793  tz9.1regs  35802  trssfir1omregs  35804  gblacfnacd  35881  onvf1odlem1  35882  onvf1odlem4  35885  vonf1oonfo  35898  erdszelem8  35963  cvmsss2  36039  cvmfolem  36044  fmlasucdisj  36164  satfun  36176  dfon2lem8  36552  dfon2lem9  36553  dfon2  36554  rdgprc  36556  nn0prpwlem  37110  ntruni  37115  clsint2  37117  fneint  37136  fnessref  37145  refssfne  37146  neibastop1  37147  neibastop2lem  37148  mh-inf3f1  37329  bj-0int  38022  bj-ismooredr  38030  relowlpssretop  38288  fvineqsneu  38335  fvineqsneq  38336  heicant  38574  mblfinlem1  38576  ftc2nc  38621  sdclem2  38677  fdc  38680  seqpo  38682  prdsbnd  38728  heibor  38756  rrnequiv  38770  0idl  38960  intidl  38964  unichnidl  38966  prnc  39002  refressn  39466  lsmcv2  40087  lcvexchlem4  40095  lcvexchlem5  40096  eqlkr  40157  paddclN  40900  pclfinN  40958  ldilcnv  41173  ldilco  41174  cdleme25dN  41414  cdlemj2  41880  tendocan  41882  erng1lem  42045  erngdvlem4-rN  42057  dihord2pre  42283  dihglblem2N  42352  dochvalr  42415  hdmap14lem12  42937  hdmap14lem13  42938  supinf  43294  fsuppind  43619  pellfundre  43888  pellfundge  43889  pellfundlb  43891  dford3lem1  44033  aomclem2  44057  oaabsb  44296  cantnf2  44327  ofoafg  44356  naddcnff  44364  naddwordnexlem3  44401  naddwordnexlem4  44403  pwinfi3  44564  iunrelexp0  44702  iunrelexpmin1  44708  iunrelexpmin2  44712  dftrcl3  44720  cnvtrclfv  44724  trclimalb2  44726  dfrtrcl3  44733  ntrneiel2  45086  ntrneik4w  45100  ntrrn  45122  gneispa  45130  gneispb  45131  addrcom  45457  iunconnlem2  45917  ssuzfz  46361  dvnprodlem3  46958  funressnfv  48113  cfsetsnfsetfo  48130  tz6.12-afv  48243  tz6.12-afv2  48310  otiunsndisjX  48349  uniimaprimaeqfv  48464  iccpartltu  48507  iccpartgtl  48508  iccpartleu  48510  iccpartgel  48511  fargshiftf  48522  fargshiftfva  48525  sbgoldbst  48876  bgoldbtbnd  48907  tgblthelfgott  48913  grimuhgr  48985  grimco  48987  isuspgrim0  48992  isuspgrimlem  48993  upgrimpths  49007  gricushgr  49015  grtriclwlk3  49043  stgr0  49058  uspgrlim  49090  grlicsym  49111  nnsgrp  49274  ellcoellss  49547  lindsrng01  49580  suppdm  49622  nn0sumshdiglem1  49733