Theorem basfn 13260

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 13259	. 2 ⊢ (Base = Slot (Base‘ndx) ∧ (Base‘ndx) ∈ ℕ)
2	1	slotslfn 13227	1 ⊢ Base Fn V

Syntax hints:  Vcvv 2812   Fn wfn 5346  Basecbs 13201

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-cnex 8214  ax-resscn 8215  ax-1re 8217  ax-addrcl 8220

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-sbc 3042  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-int 3949  df-br 4109  df-opab 4171  df-mpt 4172  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-iota 5311  df-fun 5353  df-fn 5354  df-fv 5359  df-inn 9234  df-ndx 13204  df-slot 13205  df-base 13207

This theorem is referenced by:  basmex  13261  basmexd  13262  ressbas2d  13270  ressbasid  13272  strressid  13273  ressval3d  13274  prdsex  13471  prdsval  13475  prdsbaslemss  13476  prdsbas  13478  prdsplusg  13479  prdsmulr  13480  pwsbas  13494  pwselbasb  13495  pwssnf1o  13500  imasex  13507  imasival  13508  imasbas  13509  imasplusg  13510  imasmulr  13511  imasaddfn  13519  imasaddval  13520  imasaddf  13521  imasmulfn  13522  imasmulval  13523  imasmulf  13524  qusval  13525  qusex  13527  qusaddvallemg  13535  qusaddflemg  13536  qusaddval  13537  qusaddf  13538  qusmulval  13539  qusmulf  13540  xpsval  13554  ismgm  13559  ismgmn0  13560  plusffvalg  13564  grpidvalg  13575  fn0g  13577  gsumress  13597  issgrp  13605  ismnddef  13620  issubmnd  13644  ress0g  13645  ismhm  13663  mhmex  13664  issubm  13674  grppropstrg  13721  grpinvfvalg  13744  grpinvval  13745  grpinvfng  13746  grpsubfvalg  13747  grpsubval  13748  grpressid  13763  grplactfval  13803  qusgrp2  13819  mulgfvalg  13827  mulgval  13828  mulgex  13829  mulgfng  13830  issubg  13879  subgex  13882  issubg2m  13895  isnsg  13908  releqgg  13926  eqgex  13927  eqgfval  13928  eqgen  13933  isghm  13949  ablressid  14041  isrng  14067  rngressid  14087  qusrng  14091  issrg  14098  isring  14133  ringidss  14162  ringressid  14196  qusring2  14199  dvdsrvald  14227  dvdsrex  14232  unitgrp  14250  unitabl  14251  invrfvald  14256  unitlinv  14260  unitrinv  14261  dvrfvald  14267  rdivmuldivd  14278  invrpropdg  14283  dfrhm2  14288  rhmex  14291  rhmunitinv  14312  isnzr2  14318  issubrng  14333  issubrg  14355  subrgugrp  14374  rrgval  14396  isdomn  14404  aprval  14417  aprap  14421  islmod  14426  scaffvalg  14441  rmodislmod  14486  lssex  14489  lsssetm  14491  islssm  14492  islssmg  14493  islss3  14514  lspfval  14523  lspval  14525  lspcl  14526  lspex  14530  sraval  14572  sralemg  14573  srascag  14577  sravscag  14578  sraipg  14579  sraex  14581  qusrhm  14663  psrval  14801  fnpsr  14802  psrbasg  14816  psrelbas  14817  psrplusgg  14820  psraddcl  14822  psr0cl  14823  psrnegcl  14825  psr1clfi  14830  mplvalcoe  14832  fnmpl  14835  mplplusgg  14845  vtxvalg  15998  vtxex  16000