Theorem basfn 13411

Description: The base set extractor is a function on _V. (Contributed by Stefan O'Rear, 8-Jul-2015.)

Assertion

Ref	Expression
basfn	|- Base Fn _V

Proof of Theorem basfn

Step	Hyp	Ref	Expression
1		baseslid 13410	. 2 |- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
2	1	slotslfn 13378	1 |- Base Fn _V

This proof depends on syntax axioms:   _Vcvv 2821   Fn wfn 5372   Basecbs 13352

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-iota 5337  df-fun 5379  df-fn 5380  df-fv 5385  df-inn 9305  df-ndx 13355  df-slot 13356  df-base 13358

This theorem is used by:  basmex  13412  basmexd  13413  ressbas2d  13422  ressbasid  13424  strressid  13425  ressval3d  13426  imasex  13626  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfn  13638  imasaddval  13639  imasaddf  13640  imasmulfn  13641  imasmulval  13642  imasmulf  13643  qusval  13644  qusex  13646  qusaddvallemg  13654  qusaddflemg  13655  qusaddval  13656  qusaddf  13657  qusmulval  13658  qusmulf  13659  ismgm  13677  ismgmn0  13678  plusffvalg  13682  grpidvalg  13693  fn0g  13695  gzsumress  13712  issgrp  13718  ismnddef  13731  issubmnd  13755  ress0g  13756  ismhm  13768  mhmex  13769  issubm  13779  grppropstrg  13824  grpinvfvalg  13847  grpinvval  13848  grpinvfng  13849  grpsubfvalg  13850  grpsubval  13851  grpressid  13866  grplactfval  13906  qusgrp2  13916  mulgfvalg  13924  mulgval  13925  mulgex  13926  mulgfng  13927  issubg  13976  subgex  13979  issubg2m  13992  isnsg  14005  releqgg  14023  eqgex  14024  eqgfval  14025  eqgen  14030  isghm  14046  ablressid  14139  prdsex  14172  prdsval  14173  prdsbaslemss  14174  prdsbas  14176  prdsplusg  14177  prdsmulr  14178  xpsval  14201  pwsbas  14205  pwselbasb  14206  pwssnf1o  14211  isrng  14233  rngressid  14253  qusrng  14257  issrg  14269  isring  14304  ringidss  14334  ringressid  14368  qusring2  14371  dvdsrvald  14400  dvdsrex  14405  unitgrp  14423  unitabl  14424  invrfvald  14429  unitlinv  14433  unitrinv  14434  dvrfvald  14440  rdivmuldivd  14451  invrpropdg  14456  dfrhm2  14461  rhmex  14464  rhmunitinv  14485  isnzr2  14491  issubrng  14507  issubrg  14529  subrgugrp  14548  rrgval  14570  isdomn  14578  aprval  14591  aprap  14598  aprprop  14601  islmod  14627  scaffvalg  14643  rmodislmod  14688  lssex  14691  lsssetm  14693  islssm  14694  islssmg  14695  islss3  14716  lspfval  14725  lspval  14727  lspcl  14728  lspex  14732  sraval  14774  sralemg  14775  srascag  14779  sravscag  14780  sraipg  14781  sraex  14783  qusrhm  14865  aspval  15015  asclfval  15021  psrval  15050  fnpsr  15051  psrbasg  15065  psrelbas  15066  psrplusgg  15069  psraddcl  15071  psr0cl  15072  psrnegcl  15074  psr1clfi  15079  mplvalcoe  15081  fnmpl  15084  mplplusgg  15094  vtxvalg  16257  vtxex  16259