Theorem ralrimiv 3128

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  ralrimiva  3129  ralrimivw  3133  ralrimdv  3135  ralrimivv  3178  rr19.3v  3609  class2seteq  3650  rabssdv  4014  rzalALT  4435  r19.3rzv  4443  disjord  5074  disjiund  5076  trun  5203  trin  5204  ralxfrALT  5357  otiunsndisj  5474  onmindif  6417  fnprb  7163  fntpb  7164  f1cdmsn  7237  ssorduni  7733  onminex  7756  onmindif2  7761  limuni3  7803  frxp  8076  poxp  8078  sexp2  8096  sexp3  8103  onfununi  8281  onnseq  8284  tfrlem12  8328  tz7.48-2  8381  oaass  8496  omass  8515  oelim2  8531  oelimcl  8536  oaabs2  8585  omabs  8587  uniqs  8720  undifixp  8882  dom2lem  8939  isinf  9175  unblem4  9205  unbnn2  9207  marypha1lem  9346  supssd  9376  supiso  9389  infssd  9407  ordiso2  9430  card2inf  9470  elirrvOLD  9513  wemapwe  9618  ttrclss  9641  trcl  9649  frr3g  9680  tz9.13  9715  rankval3b  9750  rankunb  9774  rankuni2b  9777  scott0  9810  updjud  9858  dfac8alem  9951  carduniima  10018  alephsmo  10024  alephval3  10032  iunfictbso  10036  dfac3  10043  dfac5lem5  10049  dfac12r  10069  dfac12k  10070  kmlem4  10076  kmlem11  10083  cfsuc  10179  cofsmo  10191  cfsmolem  10192  coftr  10195  alephsing  10198  infpssrlem3  10227  fin23lem30  10264  isf32lem2  10276  isf32lem3  10277  isf34lem6  10302  fin1a2lem11  10332  fin1a2lem13  10334  fin1a2s  10336  axcc2lem  10358  domtriomlem  10364  axdc3lem2  10373  axdc4lem  10377  axcclem  10379  axdclem2  10442  iundom2g  10462  uniimadom  10466  cardmin  10486  alephval2  10495  alephreg  10505  fpwwe2lem11  10564  wunex2  10661  wuncval2  10670  tskwe2  10696  inar1  10698  tskuni  10706  gruun  10729  intgru  10737  grutsk1  10744  genpcl  10931  ltexprlem5  10963  suplem1pr  10975  supexpr  10977  supsrlem  11034  axpre-sup  11092  negfi  12105  supaddc  12123  supadd  12124  supmul1  12125  supmullem1  12126  supmul  12128  peano5nni  12177  uzind  12621  zindd  12630  uzwo  12861  lbzbi  12886  xrsupsslem  13259  xrinfmsslem  13260  supxrun  13268  supxrpnf  13270  supxrunb1  13271  supxrunb2  13272  icoshftf1o  13427  flval3  13774  axdc4uzlem  13945  tpfo  14462  wrdnfi  14510  ccatrn  14552  ccatalpha  14556  2cshw  14775  cshweqrep  14783  s3iunsndisj  14930  rtrclreclem4  15023  dfrtrcl2  15024  01sqrexlem1  15204  01sqrexlem6  15209  fsum0diag2  15745  alzdvds  16289  gcdcllem1  16468  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  maxprmfct  16679  hashgcdeq  16760  unbenlem  16879  vdwlem6  16957  vdwlem10  16961  firest  17395  mrieqv2d  17605  iscatd  17639  initoeu2  17983  setcmon  18054  setcepi  18055  fullestrcsetc  18117  fullsetcestrc  18132  isglbd  18475  isacs4lem  18510  acsfiindd  18519  acsmapd  18520  psss  18546  sgrpidmnd  18707  pwmnd  18908  ghmrn  19204  ghmpreima  19213  cntz2ss  19310  symgextres  19400  psgnunilem2  19470  lsmsubg  19629  efgsfo  19714  gsumzaddlem  19896  gsummptnn0fzfv  19962  dmdprdd  19976  dprd2da  20019  ablsimpgprmd  20092  imasring  20310  01eq0ring  20507  isabvd  20789  issrngd  20832  islssd  20930  lbsextlem3  21158  lbsextlem4  21159  lidldvgen  21332  pzriprnglem4  21464  pzriprnglem7  21467  pzriprnglem13  21473  psgnghm  21560  isphld  21634  frlmsslsp  21776  mp2pm2mplem4  22774  tgcl  22934  distop  22960  indistopon  22966  pptbas  22973  toponmre  23058  opnnei  23085  neiuni  23087  neindisj2  23088  ordtrest2  23169  cnpnei  23229  cnindis  23257  cmpcld  23367  uncmp  23368  hauscmplem  23371  2ndc1stc  23416  1stcrest  23418  1stcelcls  23426  llyrest  23450  nllyrest  23451  cldllycmp  23460  reftr  23479  locfincf  23496  comppfsc  23497  txcls  23569  ptpjcn  23576  ptclsg  23580  dfac14lem  23582  xkoccn  23584  txlly  23601  txnlly  23602  ptrescn  23604  tx1stc  23615  xkoco1cn  23622  xkoco2cn  23623  xkococn  23625  xkoinjcn  23652  qtopeu  23681  hmeofval  23723  ordthmeolem  23766  isfild  23823  fbasrn  23849  trfil2  23852  flimclslem  23949  fclsrest  23989  fclscf  23990  flimfcls  23991  alexsubALTlem1  24012  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALT  24016  qustgpopn  24085  isxmetd  24291  imasdsf1olem  24338  blcls  24471  prdsxmslem2  24494  metustfbas  24522  dscmet  24537  nrmmetd  24539  reperflem  24784  reconnlem2  24793  xrge0tsms  24800  fsumcn  24837  cnheibor  24922  tcphcph  25204  lmmbr  25225  caubl  25275  ivthlem1  25418  ovolctb  25457  ovoliunlem2  25470  ovolscalem1  25480  ovolicc2  25489  voliunlem3  25519  ismbfd  25606  mbfimaopnlem  25622  itg2le  25706  ellimc2  25844  c1liplem1  25963  plyeq0lem  26175  dgreq0  26230  aannenlem1  26294  pilem2  26417  cxpcn3lem  26711  scvxcvx  26949  musum  27154  fsumdvdsmul  27158  dchrisum0flb  27473  ostth2lem2  27597  ltsval2  27620  nolesgn2ores  27636  nogesgn1ores  27638  nosupres  27671  nosupbnd2lem1  27679  noinfres  27686  noinfbnd2lem1  27694  cutsun12  27782  madebdayim  27880  precsexlem9  28207  addonbday  28271  noseqind  28284  z12zsodd  28474  numedglnl  29213  upgrreslem  29373  umgrreslem  29374  nbuhgr  29412  nbumgr  29416  uhgrnbgr0nb  29423  nbusgrf1o0  29438  uvtxnbgrvtx  29462  cusgrfilem2  29525  uspgr2wlkeq  29714  wwlks  29903  iswwlksnon  29921  rusgr0edg  30044  clwwlkccatlem  30059  clwwisshclwwslem  30084  clwwlkn  30096  clwwlknon  30160  3cyclfrgrrn  30356  vdgn1frgrv3  30367  2wspmdisj  30407  numclwlk2lem2f1o  30449  frgrregord013  30465  htthlem  30988  ocsh  31354  shintcli  31400  pjss2coi  32235  pjnormssi  32239  pjclem4  32270  pj3si  32278  pj3cor1i  32280  strlem3a  32323  strb  32329  hstrlem3a  32331  hstrbi  32337  spansncv2  32364  mdsl1i  32392  cvmdi  32395  mdexchi  32406  h1da  32420  mdsymlem6  32479  sumdmdii  32486  dmdbr5ati  32493  isoun  32775  xrge0tsmsd  33134  ordtrest2NEW  34067  pwsiga  34274  measiun  34362  dya2iocuni  34427  bnj518  35028  bnj1137  35137  bnj1136  35139  bnj1413  35177  bnj1417  35183  bnj60  35204  rankval4b  35243  r1filim  35247  trssfir1om  35255  fineqvnttrclselem3  35267  fineqvinfep  35269  tz9.1regs  35278  trssfir1omregs  35280  gblacfnacd  35284  onvf1odlem1  35285  onvf1odlem4  35288  subgrwlk  35314  erdszelem8  35380  cvmsss2  35456  cvmfolem  35461  fmlasucdisj  35581  satfun  35593  dfon2lem8  35970  dfon2lem9  35971  dfon2  35972  rdgprc  35974  nn0prpwlem  36504  ntruni  36509  clsint2  36511  fneint  36530  fnessref  36539  refssfne  36540  neibastop1  36541  neibastop2lem  36542  mh-inf3f1  36723  bj-0int  37413  bj-ismooredr  37421  relowlpssretop  37680  fvineqsneu  37727  fvineqsneq  37728  heicant  37976  mblfinlem1  37978  ftc2nc  38023  sdclem2  38063  fdc  38066  seqpo  38068  prdsbnd  38114  heibor  38142  rrnequiv  38156  0idl  38346  intidl  38350  unichnidl  38352  prnc  38388  refressn  38854  lsmcv2  39475  lcvexchlem4  39483  lcvexchlem5  39484  eqlkr  39545  paddclN  40288  pclfinN  40346  ldilcnv  40561  ldilco  40562  cdleme25dN  40802  cdlemj2  41268  tendocan  41270  erng1lem  41433  erngdvlem4-rN  41445  dihord2pre  41671  dihglblem2N  41740  dochvalr  41803  hdmap14lem12  42325  hdmap14lem13  42326  supinf  42681  fsuppind  43023  pellfundre  43309  pellfundge  43310  pellfundlb  43312  dford3lem1  43454  aomclem2  43483  oaabsb  43722  cantnf2  43753  ofoafg  43782  naddcnff  43790  naddwordnexlem3  43827  naddwordnexlem4  43829  pwinfi3  43990  iunrelexp0  44129  iunrelexpmin1  44135  iunrelexpmin2  44139  dftrcl3  44147  cnvtrclfv  44151  trclimalb2  44153  dfrtrcl3  44160  ntrneiel2  44513  ntrneik4w  44527  ntrrn  44549  gneispa  44557  gneispb  44558  addrcom  44901  iunconnlem2  45361  ssuzfz  45779  dvnprodlem3  46376  funressnfv  47491  cfsetsnfsetfo  47508  tz6.12-afv  47621  tz6.12-afv2  47688  otiunsndisjX  47727  uniimaprimaeqfv  47842  iccpartltu  47885  iccpartgtl  47886  iccpartleu  47888  iccpartgel  47889  fargshiftf  47900  fargshiftfva  47903  sbgoldbst  48254  bgoldbtbnd  48285  tgblthelfgott  48291  grimuhgr  48363  grimco  48365  isuspgrim0  48370  isuspgrimlem  48371  upgrimpths  48385  gricushgr  48393  grtriclwlk3  48421  stgr0  48436  uspgrlim  48468  grlicsym  48489  nnsgrp  48653  ellcoellss  48911  lindsrng01  48944  suppdm  48986  nn0sumshdiglem1  49097  setrec2fun  50167