Theorem basfn 13086

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

Syntax hints:   _Vcvv 2799   Fn wfn 5312   Basecbs 13027

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-iota 5277  df-fun 5319  df-fn 5320  df-fv 5325  df-inn 9107  df-ndx 13030  df-slot 13031  df-base 13033

This theorem is referenced by:  basmex  13087  basmexd  13088  ressbas2d  13096  ressbasid  13098  strressid  13099  ressval3d  13100  prdsex  13297  prdsval  13301  prdsbaslemss  13302  prdsbas  13304  prdsplusg  13305  prdsmulr  13306  pwsbas  13320  pwselbasb  13321  pwssnf1o  13326  imasex  13333  imasival  13334  imasbas  13335  imasplusg  13336  imasmulr  13337  imasaddfn  13345  imasaddval  13346  imasaddf  13347  imasmulfn  13348  imasmulval  13349  imasmulf  13350  qusval  13351  qusex  13353  qusaddvallemg  13361  qusaddflemg  13362  qusaddval  13363  qusaddf  13364  qusmulval  13365  qusmulf  13366  xpsval  13380  ismgm  13385  ismgmn0  13386  plusffvalg  13390  grpidvalg  13401  fn0g  13403  gsumress  13423  issgrp  13431  ismnddef  13446  issubmnd  13470  ress0g  13471  ismhm  13489  mhmex  13490  issubm  13500  grppropstrg  13547  grpinvfvalg  13570  grpinvval  13571  grpinvfng  13572  grpsubfvalg  13573  grpsubval  13574  grpressid  13589  grplactfval  13629  qusgrp2  13645  mulgfvalg  13653  mulgval  13654  mulgex  13655  mulgfng  13656  issubg  13705  subgex  13708  issubg2m  13721  isnsg  13734  releqgg  13752  eqgex  13753  eqgfval  13754  eqgen  13759  isghm  13775  ablressid  13867  isrng  13892  rngressid  13912  qusrng  13916  issrg  13923  isring  13958  ringidss  13987  ringressid  14021  qusring2  14024  reldvdsrsrg  14050  dvdsrvald  14051  dvdsrex  14056  unitgrp  14074  unitabl  14075  invrfvald  14080  unitlinv  14084  unitrinv  14085  dvrfvald  14091  rdivmuldivd  14102  invrpropdg  14107  dfrhm2  14112  rhmex  14115  rhmunitinv  14136  isnzr2  14142  issubrng  14157  issubrg  14179  subrgugrp  14198  rrgval  14220  isdomn  14227  aprval  14240  aprap  14244  islmod  14249  scaffvalg  14264  rmodislmod  14309  lssex  14312  lsssetm  14314  islssm  14315  islssmg  14316  islss3  14337  lspfval  14346  lspval  14348  lspcl  14349  lspex  14353  sraval  14395  sralemg  14396  srascag  14400  sravscag  14401  sraipg  14402  sraex  14404  qusrhm  14486  psrval  14624  fnpsr  14625  psrbasg  14632  psrelbas  14633  psrplusgg  14636  psraddcl  14638  psr0cl  14639  psrnegcl  14641  psr1clfi  14646  mplvalcoe  14648  fnmpl  14651  mplplusgg  14661  vtxvalg  15811  vtxex  15813