Theorem ralrimiv 3138

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 3137	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

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

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 1913

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

This theorem is referenced by:  ralrimiva  3139  ralrimivw  3143  ralrimdv  3145  reximdvaiOLD  3159  ralrimivv  3191  raleleq  3315  rr19.3v  3622  class2seteq  3665  rabssdv  4037  rzalALT  4472  disjord  5098  disjiund  5100  trin  5239  ralxfrALT  5375  otiunsndisj  5482  onmindif  6414  fnprb  7163  fntpb  7164  f1cdmsn  7233  ssorduni  7718  onminex  7742  onmindif2  7747  sucexeloniOLD  7750  suceloniOLD  7752  limuni3  7793  frxp  8063  poxp  8065  sexp2  8083  sexp3  8090  wfrlem15OLD  8274  onfununi  8292  onnseq  8295  tfrlem12  8340  tz7.48-2  8393  oaass  8513  omass  8532  oelim2  8547  oelimcl  8552  oaabs2  8600  omabs  8602  undifixp  8879  dom2lem  8939  isinf  9211  isinfOLD  9212  unblem4  9249  unbnn2  9251  marypha1lem  9378  supiso  9420  ordiso2  9460  card2inf  9500  elirrv  9541  wemapwe  9642  ttrclss  9665  trcl  9673  frr3g  9701  tz9.13  9736  rankval3b  9771  rankunb  9795  rankuni2b  9798  scott0  9831  updjud  9879  dfac8alem  9974  carduniima  10041  alephsmo  10047  alephval3  10055  iunfictbso  10059  dfac3  10066  dfac5lem5  10072  dfac12r  10091  dfac12k  10092  kmlem4  10098  kmlem11  10105  cfsuc  10202  cofsmo  10214  cfsmolem  10215  coftr  10218  alephsing  10221  infpssrlem3  10250  fin23lem30  10287  isf32lem2  10299  isf32lem3  10300  isf34lem6  10325  fin1a2lem11  10355  fin1a2lem13  10357  fin1a2s  10359  axcc2lem  10381  domtriomlem  10387  axdc3lem2  10396  axdc4lem  10400  axcclem  10402  axdclem2  10465  iundom2g  10485  uniimadom  10489  cardmin  10509  alephval2  10517  alephreg  10527  fpwwe2lem11  10586  wunex2  10683  wuncval2  10692  tskwe2  10718  inar1  10720  tskuni  10728  gruun  10751  intgru  10759  grutsk1  10766  genpcl  10953  ltexprlem5  10985  suplem1pr  10997  supexpr  10999  supsrlem  11056  axpre-sup  11114  negfi  12113  supaddc  12131  supadd  12132  supmul1  12133  supmullem1  12134  supmul  12136  peano5nni  12165  uzind  12604  zindd  12613  uzwo  12845  lbzbi  12870  xrsupsslem  13236  xrinfmsslem  13237  supxrun  13245  supxrpnf  13247  supxrunb1  13248  supxrunb2  13249  icoshftf1o  13401  flval3  13730  axdc4uzlem  13898  wrdnfi  14448  ccatrn  14489  ccatalpha  14493  2cshw  14713  cshweqrep  14721  s3iunsndisj  14865  rtrclreclem4  14958  dfrtrcl2  14959  01sqrexlem1  15139  01sqrexlem6  15144  fsum0diag2  15679  alzdvds  16213  gcdcllem1  16390  lcmfunsnlem2lem1  16525  lcmfunsnlem2lem2  16526  maxprmfct  16596  hashgcdeq  16672  unbenlem  16791  vdwlem6  16869  vdwlem10  16873  firest  17328  mrieqv2d  17533  iscatd  17567  initoeu2  17916  setcmon  17987  setcepi  17988  fullestrcsetc  18053  fullsetcestrc  18068  isglbd  18412  isacs4lem  18447  acsfiindd  18456  acsmapd  18457  psss  18483  sgrpidmnd  18575  pwmnd  18761  ghmrn  19035  ghmpreima  19044  cntz2ss  19127  symgextres  19221  psgnunilem2  19291  lsmsubg  19450  efgsfo  19535  gsumzaddlem  19712  gsummptnn0fzfv  19778  dmdprdd  19792  dprd2da  19835  ablsimpgprmd  19908  imasring  20059  01eq0ring  20215  isabvd  20335  issrngd  20376  islssd  20453  lbsextlem3  20680  lbsextlem4  20681  lidldvgen  20784  psgnghm  21021  isphld  21095  frlmsslsp  21239  mp2pm2mplem4  22195  tgcl  22356  distop  22382  indistopon  22388  pptbas  22395  toponmre  22481  opnnei  22508  neiuni  22510  neindisj2  22511  ordtrest2  22592  cnpnei  22652  cnindis  22680  cmpcld  22790  uncmp  22791  hauscmplem  22794  2ndc1stc  22839  1stcrest  22841  1stcelcls  22849  llyrest  22873  nllyrest  22874  cldllycmp  22883  reftr  22902  locfincf  22919  comppfsc  22920  txcls  22992  ptpjcn  22999  ptclsg  23003  dfac14lem  23005  xkoccn  23007  txlly  23024  txnlly  23025  ptrescn  23027  tx1stc  23038  xkoco1cn  23045  xkoco2cn  23046  xkococn  23048  xkoinjcn  23075  qtopeu  23104  hmeofval  23146  ordthmeolem  23189  isfild  23246  fbasrn  23272  trfil2  23275  flimclslem  23372  fclsrest  23412  fclscf  23413  flimfcls  23414  alexsubALTlem1  23435  alexsubALTlem2  23436  alexsubALTlem3  23437  alexsubALT  23439  qustgpopn  23508  isxmetd  23716  imasdsf1olem  23763  blcls  23899  prdsxmslem2  23922  metustfbas  23950  dscmet  23965  nrmmetd  23967  reperflem  24218  reconnlem2  24227  xrge0tsms  24234  fsumcn  24270  cnheibor  24355  tcphcph  24638  lmmbr  24659  caubl  24709  ivthlem1  24852  ovolctb  24891  ovoliunlem2  24904  ovolscalem1  24914  ovolicc2  24923  voliunlem3  24953  ismbfd  25040  mbfimaopnlem  25056  itg2le  25141  ellimc2  25278  c1liplem1  25397  plyeq0lem  25608  dgreq0  25663  aannenlem1  25725  pilem2  25848  cxpcn3lem  26137  scvxcvx  26372  musum  26577  dchrisum0flb  26895  ostth2lem2  27019  sltval2  27041  nolesgn2ores  27057  nogesgn1ores  27059  nosupres  27092  nosupbnd2lem1  27100  noinfres  27107  noinfbnd2lem1  27115  scutun12  27192  madebdayim  27260  numedglnl  28158  upgrreslem  28315  umgrreslem  28316  nbuhgr  28354  nbumgr  28358  uhgrnbgr0nb  28365  nbusgrf1o0  28380  uvtxnbgrvtx  28404  cusgrfilem2  28467  uspgr2wlkeq  28657  wwlks  28843  iswwlksnon  28861  rusgr0edg  28981  clwwlkccatlem  28996  clwwisshclwwslem  29021  clwwlkn  29033  clwwlknon  29097  3cyclfrgrrn  29293  vdgn1frgrv3  29304  2wspmdisj  29344  numclwlk2lem2f1o  29386  frgrregord013  29402  htthlem  29922  ocsh  30288  shintcli  30334  pjss2coi  31169  pjnormssi  31173  pjclem4  31204  pj3si  31212  pj3cor1i  31214  strlem3a  31257  strb  31263  hstrlem3a  31265  hstrbi  31271  spansncv2  31298  mdsl1i  31326  cvmdi  31329  mdexchi  31340  h1da  31354  mdsymlem6  31413  sumdmdii  31420  dmdbr5ati  31427  isoun  31683  supssd  31694  infssd  31695  xrge0tsmsd  31969  ordtrest2NEW  32593  pwsiga  32818  measiun  32906  dya2iocuni  32972  bnj518  33587  bnj1137  33696  bnj1136  33698  bnj1413  33736  bnj1417  33742  bnj60  33763  subgrwlk  33813  erdszelem8  33879  cvmsss2  33955  cvmfolem  33960  fmlasucdisj  34080  satfun  34092  dfon2lem8  34451  dfon2lem9  34452  dfon2  34453  rdgprc  34455  nn0prpwlem  34870  ntruni  34875  clsint2  34877  fneint  34896  fnessref  34905  refssfne  34906  neibastop1  34907  neibastop2lem  34908  bj-0int  35645  bj-ismooredr  35653  relowlpssretop  35908  fvineqsneu  35955  fvineqsneq  35956  heicant  36186  mblfinlem1  36188  ftc2nc  36233  sdclem2  36274  fdc  36277  seqpo  36279  prdsbnd  36325  heibor  36353  rrnequiv  36367  0idl  36557  intidl  36561  unichnidl  36563  prnc  36599  uniqsALTV  36863  refressn  36978  lsmcv2  37564  lcvexchlem4  37572  lcvexchlem5  37573  eqlkr  37634  paddclN  38378  pclfinN  38436  ldilcnv  38651  ldilco  38652  cdleme25dN  38892  cdlemj2  39358  tendocan  39360  erng1lem  39523  erngdvlem4-rN  39535  dihord2pre  39761  dihglblem2N  39830  dochvalr  39893  hdmap14lem12  40415  hdmap14lem13  40416  fsuppind  40823  pellfundre  41262  pellfundge  41263  pellfundlb  41265  dford3lem1  41408  aomclem2  41440  oaabsb  41687  cantnf2  41718  ofoafg  41747  naddcnff  41755  naddwordnexlem3  41793  naddwordnexlem4  41795  pwinfi3  41957  iunrelexp0  42096  iunrelexpmin1  42102  iunrelexpmin2  42106  dftrcl3  42114  cnvtrclfv  42118  trclimalb2  42120  dfrtrcl3  42127  ntrneiel2  42480  ntrneik4w  42494  ntrrn  42516  gneispa  42524  gneispb  42525  addrcom  42877  iunconnlem2  43339  ssuzfz  43704  dvmptfprod  44306  dvnprodlem3  44309  funressnfv  45397  cfsetsnfsetfo  45414  tz6.12-afv  45525  tz6.12-afv2  45592  otiunsndisjX  45631  uniimaprimaeqfv  45694  iccpartltu  45737  iccpartgtl  45738  iccpartleu  45740  iccpartgel  45741  fargshiftf  45752  fargshiftfva  45755  sbgoldbst  46090  bgoldbtbnd  46121  tgblthelfgott  46127  isomushgr  46138  nnsgrp  46231  ellcoellss  46636  lindsrng01  46669  suppdm  46711  nn0sumshdiglem1  46827  setrec2fun  47257