Theorem basfn 13470

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

This proof depends on syntax axioms:  Vcvv 2821   Fn wfn 5375  Basecbs 13411

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-cnex 8277  ax-resscn 8278  ax-1re 8280  ax-addrcl 8283

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-iota 5340  df-fun 5382  df-fn 5383  df-fv 5388  df-inn 9315  df-ndx 13414  df-slot 13415  df-base 13417

This theorem is used by:  basmex  13471  basmexd  13472  ressbas2d  13482  ressbasid  13484  strressid  13485  ressval3d  13486  imasex  13686  imasival  13687  imasbas  13688  imasplusg  13689  imasmulr  13690  imasaddfn  13698  imasaddval  13699  imasaddf  13700  imasmulfn  13701  imasmulval  13702  imasmulf  13703  qusval  13704  qusex  13706  qusaddvallemg  13714  qusaddflemg  13715  qusaddval  13716  qusaddf  13717  qusmulval  13718  qusmulf  13719  ismgm  13737  ismgmn0  13738  plusffvalg  13742  grpidvalg  13753  fn0g  13755  gzsumress  13772  issgrp  13778  ismnddef  13791  issubmnd  13815  ress0g  13816  ismhm  13828  mhmex  13829  issubm  13839  grppropstrg  13884  grpinvfvalg  13907  grpinvval  13908  grpinvfng  13909  grpsubfvalg  13910  grpsubval  13911  grpressid  13926  grplactfval  13966  qusgrp2  13976  mulgfvalg  13984  mulgval  13985  mulgex  13986  mulgfng  13987  issubg  14036  subgex  14039  issubg2m  14052  isnsg  14065  releqgg  14083  eqgex  14084  eqgfval  14085  eqgen  14090  isghm  14106  cntzex  14151  cntrval  14152  cntzfval  14153  cntzval  14154  ablressid  14230  prdsex  14280  prdsval  14281  prdsbaslemss  14282  prdsbas  14284  prdsplusg  14285  prdsmulr  14286  xpsval  14309  pwsbas  14313  pwselbasb  14314  pwssnf1o  14319  isrng  14341  rngressid  14361  qusrng  14365  issrg  14377  isring  14412  ringidss  14442  ringressid  14478  qusring2  14481  dvdsrvald  14510  dvdsrex  14515  unitgrp  14533  unitabl  14534  invrfvald  14539  unitlinv  14543  unitrinv  14544  dvrfvald  14550  rdivmuldivd  14561  invrpropdg  14566  dfrhm2  14571  rhmex  14574  rhmunitinv  14595  isnzr2  14601  issubrng  14617  issubrg  14639  subrgugrp  14658  rrgval  14680  isdomn  14688  aprval  14701  aprap  14708  aprprop  14711  islmod  14737  scaffvalg  14753  rmodislmod  14798  lssex  14801  lsssetm  14803  islssm  14804  islssmg  14805  islss3  14826  lspfval  14835  lspval  14837  lspcl  14838  lspex  14842  sraval  14884  sralemg  14885  srascag  14889  sravscag  14890  sraipg  14891  sraex  14893  qusrhm  14975  aspval  15125  asclfval  15131  psrval  15162  fnpsr  15163  psrbasg  15183  psrelbas  15184  psrplusgg  15187  psraddcl  15189  psrmulrg  15191  psrmulclfilem  15194  psr0cl  15196  psrnegcl  15198  psr1clfi  15203  mvrffi  15214  mplvalcoe  15218  fnmpl  15221  mplplusgg  15231  vtxvalg  16474  vtxex  16476