Theorem basfn 13204

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

Syntax hints:   _Vcvv 2803   Fn wfn 5328   Basecbs 13145

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 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-iota 5293  df-fun 5335  df-fn 5336  df-fv 5341  df-inn 9186  df-ndx 13148  df-slot 13149  df-base 13151

This theorem is referenced by:  basmex  13205  basmexd  13206  ressbas2d  13214  ressbasid  13216  strressid  13217  ressval3d  13218  prdsex  13415  prdsval  13419  prdsbaslemss  13420  prdsbas  13422  prdsplusg  13423  prdsmulr  13424  pwsbas  13438  pwselbasb  13439  pwssnf1o  13444  imasex  13451  imasival  13452  imasbas  13453  imasplusg  13454  imasmulr  13455  imasaddfn  13463  imasaddval  13464  imasaddf  13465  imasmulfn  13466  imasmulval  13467  imasmulf  13468  qusval  13469  qusex  13471  qusaddvallemg  13479  qusaddflemg  13480  qusaddval  13481  qusaddf  13482  qusmulval  13483  qusmulf  13484  xpsval  13498  ismgm  13503  ismgmn0  13504  plusffvalg  13508  grpidvalg  13519  fn0g  13521  gsumress  13541  issgrp  13549  ismnddef  13564  issubmnd  13588  ress0g  13589  ismhm  13607  mhmex  13608  issubm  13618  grppropstrg  13665  grpinvfvalg  13688  grpinvval  13689  grpinvfng  13690  grpsubfvalg  13691  grpsubval  13692  grpressid  13707  grplactfval  13747  qusgrp2  13763  mulgfvalg  13771  mulgval  13772  mulgex  13773  mulgfng  13774  issubg  13823  subgex  13826  issubg2m  13839  isnsg  13852  releqgg  13870  eqgex  13871  eqgfval  13872  eqgen  13877  isghm  13893  ablressid  13985  isrng  14011  rngressid  14031  qusrng  14035  issrg  14042  isring  14077  ringidss  14106  ringressid  14140  qusring2  14143  dvdsrvald  14171  dvdsrex  14176  unitgrp  14194  unitabl  14195  invrfvald  14200  unitlinv  14204  unitrinv  14205  dvrfvald  14211  rdivmuldivd  14222  invrpropdg  14227  dfrhm2  14232  rhmex  14235  rhmunitinv  14256  isnzr2  14262  issubrng  14277  issubrg  14299  subrgugrp  14318  rrgval  14340  isdomn  14348  aprval  14361  aprap  14365  islmod  14370  scaffvalg  14385  rmodislmod  14430  lssex  14433  lsssetm  14435  islssm  14436  islssmg  14437  islss3  14458  lspfval  14467  lspval  14469  lspcl  14470  lspex  14474  sraval  14516  sralemg  14517  srascag  14521  sravscag  14522  sraipg  14523  sraex  14525  qusrhm  14607  psrval  14745  fnpsr  14746  psrbasg  14758  psrelbas  14759  psrplusgg  14762  psraddcl  14764  psr0cl  14765  psrnegcl  14767  psr1clfi  14772  mplvalcoe  14774  fnmpl  14777  mplplusgg  14787  vtxvalg  15940  vtxex  15942