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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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  4021  rzalALT  4450  r19.3rzv  4458  disjord  5091  disjiund  5093  trun  5222  trin  5223  ralxfrALT  5376  otiunsndisj  5489  onmindif  6446  fnprb  7202  fntpb  7203  f1cdmsn  7278  ssorduni  7776  onminex  7799  onmindif2  7804  limuni3  7846  frxp  8121  poxp  8123  sexp2  8141  sexp3  8148  onfununi  8327  onnseq  8330  tfrlem12  8375  tz7.48-2  8430  oaass  8547  omass  8566  oelim2  8582  oelimcl  8587  oaabs2  8636  omabs  8638  uniqs  8772  undifixp  8940  dom2lem  8997  isinf  9234  unblem4  9265  unbnn2  9267  marypha1lem  9403  supssd  9433  supiso  9446  infssd  9464  ordiso2  9487  card2inf  9527  elirrvOLDOLD  9571  wemapwe  9676  ttrclss  9699  trcl  9707  frr3g  9738  tz9.13  9773  rankval3b  9809  rankunb  9837  rankuni2b  9840  rankval4b  9853  elhf4  9883  scott0b  9908  scott0OLD  9909  setrec2fun  9944  updjud  9986  dfac8alem  10079  carduniima  10146  alephsmo  10152  alephval3  10160  iunfictbso  10164  dfac3  10171  dfac5lem5  10177  dfac12r  10196  dfac12k  10197  kmlem4  10203  kmlem11  10210  cfsuc  10306  cofsmo  10318  cfsmolem  10319  coftr  10322  alephsing  10325  infpssrlem3  10354  fin23lem30  10391  isf32lem2  10403  isf32lem3  10404  isf34lem6  10429  fin1a2lem11  10459  fin1a2lem13  10461  fin1a2s  10463  axcc2lem  10485  domtriomlem  10491  axdc3lem2  10500  axdc4lem  10504  axcclem  10506  axdclem2  10569  iundom2g  10595  uniimadom  10599  cardmin  10619  alephval2  10628  alephreg  10638  fpwwe2lem11  10697  wunex2  10794  wuncval2  10803  tskwe2  10829  inar1  10831  tskuni  10839  gruun  10862  intgru  10870  grutsk1  10877  genpcl  11064  ltexprlem5  11096  suplem1pr  11108  supexpr  11110  supsrlem  11167  axpre-sup  11225  negfi  12235  supaddc  12253  supadd  12254  supmul1  12255  supmullem1  12256  supmul  12258  peano5nni  12307  uzind  12760  zindd  12769  uzwo  13007  lbzbi  13032  xrsupsslem  13406  xrinfmsslem  13407  supxrun  13415  supxrpnf  13417  supxrunb1  13418  supxrunb2  13419  icoshftf1o  13574  flval3  13923  axdc4uzlem  14094  tpfo  14612  wrdnfi  14660  ccatrn  14702  ccatalpha  14707  2cshw  14931  cshweqrep  14939  s3iunsndisj  15088  rtrclreclem4  15181  dfrtrcl2  15182  01sqrexlem1  15376  01sqrexlem6  15381  fsum0diag2  15916  alzdvds  16457  gcdcllem1  16636  lcmfunsnlem2lem1  16775  lcmfunsnlem2lem2  16776  maxprmfct  16847  hashgcdeq  16928  unbenlem  17047  vdwlem6  17125  vdwlem10  17129  firest  17564  mrieqv2d  17774  iscatd  17808  initoeu2  18152  setcmon  18223  setcepi  18224  fullestrcsetc  18286  fullsetcestrc  18301  isglbd  18644  isacs4lem  18679  acsfiindd  18688  acsmapd  18689  psss  18715  mgmn0plusgf  18788  sgrpidmnd  18889  pwmnd  19104  ghmrn  19404  ghmpreima  19413  cntz2ss  19510  symgextres  19600  psgnunilem2  19670  lsmsubg  19829  efgsfo  19914  gsumzaddlem  20096  gsummptnn0fzfv  20162  dmdprdd  20176  dprd2da  20219  ablsimpgprmd  20292  imasring  20521  01eq0ring  20742  isabvd  21030  issrngd  21073  islssd  21171  lbsextlem3  21399  lbsextlem4  21400  unichnlidl  21477  lidldvgen  21619  pzriprnglem4  21751  pzriprnglem7  21754  pzriprnglem13  21760  psgnghm  21847  isphld  21921  frlmsslsp  22063  mp2pm2mplem4  23088  tgcl  23248  distop  23274  indistopon  23280  pptbas  23287  toponmre  23372  opnnei  23399  neiuni  23401  neindisj2  23402  ordtrest2  23483  cnpnei  23543  cnindis  23571  cmpcld  23681  uncmp  23682  hauscmplem  23685  2ndc1stc  23730  1stcrest  23732  1stcelcls  23741  llyrest  23765  nllyrest  23766  cldllycmp  23775  reftr  23794  locfincf  23811  comppfsc  23812  txcls  23884  ptpjcn  23891  ptclsg  23895  dfac14lem  23897  xkoccn  23899  txlly  23916  txnlly  23917  ptrescn  23919  tx1stc  23930  xkoco1cn  23937  xkoco2cn  23938  xkococn  23940  xkoinjcn  23967  qtopeu  23996  hmeofval  24038  ordthmeolem  24081  isfild  24138  fbasrn  24164  trfil2  24167  flimclslem  24264  fclsrest  24304  fclscf  24305  flimfcls  24306  alexsubALTlem1  24327  alexsubALTlem2  24328  alexsubALTlem3  24329  alexsubALT  24331  qustgpopn  24400  isxmetd  24606  imasdsf1olem  24653  blcls  24786  prdsxmslem2  24809  metustfbas  24837  dscmet  24852  nrmmetd  24854  reperflem  25099  reconnlem2  25108  xrge0tsms  25115  fsumcn  25152  cnheibor  25237  tcphcph  25519  lmmbr  25540  caubl  25590  ivthlem1  25733  ovolctb  25772  ovoliunlem2  25785  ovolscalem1  25795  ovolicc2  25804  voliunlem3  25834  ismbfd  25921  mbfimaopnlem  25937  itg2le  26021  ellimc2  26158  c1liplem1  26277  plyeq0lem  26490  dgreq0  26545  aannenlem1  26618  pilem2  26742  cxpcn3lem  27038  scvxcvx  27276  musum  27481  fsumdvdsmul  27485  dchrisum0flb  27800  ostth2lem2  27924  ltsval2  27946  nolesgn2ores  27962  nogesgn1ores  27964  nosupres  27997  nosupbnd2lem1  28005  noinfres  28012  noinfbnd2lem1  28020  cutsun12  28109  madebdayim  28207  precsexlem9  28534  addonbday  28598  noseqind  28611  z12zsodd  28801  numedglnl  29655  upgrreslem  29818  umgrreslem  29819  nbuhgr  29857  nbumgr  29861  uhgrnbgr0nb  29868  nbusgrf1o0  29883  uvtxnbgrvtx  29907  cusgrfilem2  29970  uspgr2wlkeq  30159  subgrwlk  30202  wwlks  30357  iswwlksnon  30375  rusgr0edg  30498  clwwlkccatlem  30513  clwwisshclwwslem  30538  clwwlkn  30550  clwwlknon  30614  3cyclfrgrrn  30820  vdgn1frgrv3  30831  2wspmdisj  30871  numclwlk2lem2f1o  30913  frgrregord013  30929  htthlem  31452  ocsh  31818  shintcli  31864  pjss2coi  32699  pjnormssi  32703  pjclem4  32734  pj3si  32742  pj3cor1i  32744  strlem3a  32787  strb  32793  hstrlem3a  32795  hstrbi  32801  spansncv2  32828  mdsl1i  32856  cvmdi  32859  mdexchi  32870  h1da  32884  mdsymlem6  32943  sumdmdii  32950  dmdbr5ati  32957  isoun  33228  xrge0tsmsd  33567  ordtrest2NEW  34488  pwsiga  34695  measiun  34784  dya2iocuni  34849  bnj518  35450  bnj1137  35559  bnj1136  35561  bnj1413  35599  bnj1417  35605  bnj60  35626  r1filim  35659  trssfir1om  35668  fineqvnttrclselem3  35716  fineqvinfep  35718  tz9.1regs  35727  trssfir1omregs  35729  gblacfnacd  35806  onvf1odlem1  35807  onvf1odlem4  35810  vonf1oonfo  35819  erdszelem8  35884  cvmsss2  35960  cvmfolem  35965  fmlasucdisj  36085  satfun  36097  dfon2lem8  36474  dfon2lem9  36475  dfon2  36476  rdgprc  36478  nn0prpwlem  37032  ntruni  37037  clsint2  37039  fneint  37058  fnessref  37067  refssfne  37068  neibastop1  37069  neibastop2lem  37070  mh-inf3f1  37251  bj-0int  37942  bj-ismooredr  37950  relowlpssretop  38207  fvineqsneu  38254  fvineqsneq  38255  heicant  38493  mblfinlem1  38495  ftc2nc  38540  sdclem2  38596  fdc  38599  seqpo  38601  prdsbnd  38647  heibor  38675  rrnequiv  38689  0idl  38879  intidl  38883  unichnidl  38885  prnc  38921  refressn  39385  lsmcv2  40006  lcvexchlem4  40014  lcvexchlem5  40015  eqlkr  40076  paddclN  40819  pclfinN  40877  ldilcnv  41092  ldilco  41093  cdleme25dN  41333  cdlemj2  41799  tendocan  41801  erng1lem  41964  erngdvlem4-rN  41976  dihord2pre  42202  dihglblem2N  42271  dochvalr  42334  hdmap14lem12  42856  hdmap14lem13  42857  supinf  43213  fsuppind  43540  pellfundre  43826  pellfundge  43827  pellfundlb  43829  dford3lem1  43971  aomclem2  44000  oaabsb  44239  cantnf2  44270  ofoafg  44299  naddcnff  44307  naddwordnexlem3  44344  naddwordnexlem4  44346  pwinfi3  44507  iunrelexp0  44646  iunrelexpmin1  44652  iunrelexpmin2  44656  dftrcl3  44664  cnvtrclfv  44668  trclimalb2  44670  dfrtrcl3  44677  ntrneiel2  45030  ntrneik4w  45044  ntrrn  45066  gneispa  45074  gneispb  45075  addrcom  45401  iunconnlem2  45861  ssuzfz  46283  dvnprodlem3  46880  funressnfv  48035  cfsetsnfsetfo  48052  tz6.12-afv  48165  tz6.12-afv2  48232  otiunsndisjX  48271  uniimaprimaeqfv  48386  iccpartltu  48429  iccpartgtl  48430  iccpartleu  48432  iccpartgel  48433  fargshiftf  48444  fargshiftfva  48447  sbgoldbst  48798  bgoldbtbnd  48829  tgblthelfgott  48835  grimuhgr  48907  grimco  48909  isuspgrim0  48914  isuspgrimlem  48915  upgrimpths  48929  gricushgr  48937  grtriclwlk3  48965  stgr0  48980  uspgrlim  49012  grlicsym  49033  nnsgrp  49196  ellcoellss  49469  lindsrng01  49502  suppdm  49544  nn0sumshdiglem1  49655