Theorem basfn 12832

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 12831	. 2 |- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
2	1	slotslfn 12800	1 |- Base Fn _V

Syntax hints:   _Vcvv 2771   Fn wfn 5265   Basecbs 12774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-cnex 8015  ax-resscn 8016  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-sbc 2998  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-mpt 4106  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-res 4686  df-iota 5231  df-fun 5272  df-fn 5273  df-fv 5278  df-inn 9036  df-ndx 12777  df-slot 12778  df-base 12780

This theorem is referenced by:  basmex  12833  basmexd  12834  ressbas2d  12842  ressbasid  12844  strressid  12845  ressval3d  12846  prdsex  13043  prdsval  13047  prdsbaslemss  13048  prdsbas  13050  prdsplusg  13051  prdsmulr  13052  pwsbas  13066  pwselbasb  13067  pwssnf1o  13072  imasex  13079  imasival  13080  imasbas  13081  imasplusg  13082  imasmulr  13083  imasaddfn  13091  imasaddval  13092  imasaddf  13093  imasmulfn  13094  imasmulval  13095  imasmulf  13096  qusval  13097  qusex  13099  qusaddvallemg  13107  qusaddflemg  13108  qusaddval  13109  qusaddf  13110  qusmulval  13111  qusmulf  13112  xpsval  13126  ismgm  13131  ismgmn0  13132  plusffvalg  13136  grpidvalg  13147  fn0g  13149  gsumress  13169  issgrp  13177  ismnddef  13192  issubmnd  13216  ress0g  13217  ismhm  13235  mhmex  13236  issubm  13246  grppropstrg  13293  grpinvfvalg  13316  grpinvval  13317  grpinvfng  13318  grpsubfvalg  13319  grpsubval  13320  grpressid  13335  grplactfval  13375  qusgrp2  13391  mulgfvalg  13399  mulgval  13400  mulgex  13401  mulgfng  13402  issubg  13451  subgex  13454  issubg2m  13467  isnsg  13480  releqgg  13498  eqgex  13499  eqgfval  13500  eqgen  13505  isghm  13521  ablressid  13613  isrng  13638  rngressid  13658  qusrng  13662  issrg  13669  isring  13704  ringidss  13733  ringressid  13767  qusring2  13770  reldvdsrsrg  13796  dvdsrvald  13797  dvdsrex  13802  unitgrp  13820  unitabl  13821  invrfvald  13826  unitlinv  13830  unitrinv  13831  dvrfvald  13837  rdivmuldivd  13848  invrpropdg  13853  dfrhm2  13858  rhmex  13861  rhmunitinv  13882  isnzr2  13888  issubrng  13903  issubrg  13925  subrgugrp  13944  rrgval  13966  isdomn  13973  aprval  13986  aprap  13990  islmod  13995  scaffvalg  14010  rmodislmod  14055  lssex  14058  lsssetm  14060  islssm  14061  islssmg  14062  islss3  14083  lspfval  14092  lspval  14094  lspcl  14095  lspex  14099  sraval  14141  sralemg  14142  srascag  14146  sravscag  14147  sraipg  14148  sraex  14150  qusrhm  14232  psrval  14370  fnpsr  14371  psrbasg  14378  psrelbas  14379  psrplusgg  14382  psraddcl  14384  psr0cl  14385  psrnegcl  14387  psr1clfi  14392  mplvalcoe  14394  fnmpl  14397  mplplusgg  14407  vtxvalg  15557