Theorem basfn 12809

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

Syntax hints:   _Vcvv 2771   Fn wfn 5263   Basecbs 12751

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 4478  ax-cnex 7998  ax-resscn 7999  ax-1re 8001  ax-addrcl 8004

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 4338  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-rn 4684  df-res 4685  df-iota 5229  df-fun 5270  df-fn 5271  df-fv 5276  df-inn 9019  df-ndx 12754  df-slot 12755  df-base 12757

This theorem is referenced by:  basmex  12810  basmexd  12811  ressbas2d  12819  ressbasid  12821  strressid  12822  ressval3d  12823  prdsex  13019  prdsval  13023  prdsbaslemss  13024  prdsbas  13026  prdsplusg  13027  prdsmulr  13028  pwsbas  13042  pwselbasb  13043  pwssnf1o  13048  imasex  13055  imasival  13056  imasbas  13057  imasplusg  13058  imasmulr  13059  imasaddfn  13067  imasaddval  13068  imasaddf  13069  imasmulfn  13070  imasmulval  13071  imasmulf  13072  qusval  13073  qusex  13075  qusaddvallemg  13083  qusaddflemg  13084  qusaddval  13085  qusaddf  13086  qusmulval  13087  qusmulf  13088  xpsval  13102  ismgm  13107  ismgmn0  13108  plusffvalg  13112  grpidvalg  13123  fn0g  13125  gsumress  13145  issgrp  13153  ismnddef  13168  issubmnd  13192  ress0g  13193  ismhm  13211  mhmex  13212  issubm  13222  grppropstrg  13269  grpinvfvalg  13292  grpinvval  13293  grpinvfng  13294  grpsubfvalg  13295  grpsubval  13296  grpressid  13311  grplactfval  13351  qusgrp2  13367  mulgfvalg  13375  mulgval  13376  mulgex  13377  mulgfng  13378  issubg  13427  subgex  13430  issubg2m  13443  isnsg  13456  releqgg  13474  eqgex  13475  eqgfval  13476  eqgen  13481  isghm  13497  ablressid  13589  isrng  13614  rngressid  13634  qusrng  13638  issrg  13645  isring  13680  ringidss  13709  ringressid  13743  qusring2  13746  reldvdsrsrg  13772  dvdsrvald  13773  dvdsrex  13778  unitgrp  13796  unitabl  13797  invrfvald  13802  unitlinv  13806  unitrinv  13807  dvrfvald  13813  rdivmuldivd  13824  invrpropdg  13829  dfrhm2  13834  rhmex  13837  rhmunitinv  13858  isnzr2  13864  issubrng  13879  issubrg  13901  subrgugrp  13920  rrgval  13942  isdomn  13949  aprval  13962  aprap  13966  islmod  13971  scaffvalg  13986  rmodislmod  14031  lssex  14034  lsssetm  14036  islssm  14037  islssmg  14038  islss3  14059  lspfval  14068  lspval  14070  lspcl  14071  lspex  14075  sraval  14117  sralemg  14118  srascag  14122  sravscag  14123  sraipg  14124  sraex  14126  qusrhm  14208  psrval  14346  fnpsr  14347  psrbasg  14354  psrelbas  14355  psrplusgg  14358  psraddcl  14360  psr0cl  14361  psrnegcl  14363  psr1clfi  14368  mplvalcoe  14370  fnmpl  14373  mplplusgg  14383