Theorem basfn 13112

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

Syntax hints:  Vcvv 2799   Fn wfn 5316  Basecbs 13053

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 4202  ax-pow 4259  ax-pr 4294  ax-un 4525  ax-cnex 8106  ax-resscn 8107  ax-1re 8109  ax-addrcl 8112

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 3889  df-int 3924  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4385  df-xp 4726  df-rel 4727  df-cnv 4728  df-co 4729  df-dm 4730  df-rn 4731  df-res 4732  df-iota 5281  df-fun 5323  df-fn 5324  df-fv 5329  df-inn 9127  df-ndx 13056  df-slot 13057  df-base 13059

This theorem is referenced by:  basmex  13113  basmexd  13114  ressbas2d  13122  ressbasid  13124  strressid  13125  ressval3d  13126  prdsex  13323  prdsval  13327  prdsbaslemss  13328  prdsbas  13330  prdsplusg  13331  prdsmulr  13332  pwsbas  13346  pwselbasb  13347  pwssnf1o  13352  imasex  13359  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfn  13371  imasaddval  13372  imasaddf  13373  imasmulfn  13374  imasmulval  13375  imasmulf  13376  qusval  13377  qusex  13379  qusaddvallemg  13387  qusaddflemg  13388  qusaddval  13389  qusaddf  13390  qusmulval  13391  qusmulf  13392  xpsval  13406  ismgm  13411  ismgmn0  13412  plusffvalg  13416  grpidvalg  13427  fn0g  13429  gsumress  13449  issgrp  13457  ismnddef  13472  issubmnd  13496  ress0g  13497  ismhm  13515  mhmex  13516  issubm  13526  grppropstrg  13573  grpinvfvalg  13596  grpinvval  13597  grpinvfng  13598  grpsubfvalg  13599  grpsubval  13600  grpressid  13615  grplactfval  13655  qusgrp2  13671  mulgfvalg  13679  mulgval  13680  mulgex  13681  mulgfng  13682  issubg  13731  subgex  13734  issubg2m  13747  isnsg  13760  releqgg  13778  eqgex  13779  eqgfval  13780  eqgen  13785  isghm  13801  ablressid  13893  isrng  13918  rngressid  13938  qusrng  13942  issrg  13949  isring  13984  ringidss  14013  ringressid  14047  qusring2  14050  dvdsrvald  14078  dvdsrex  14083  unitgrp  14101  unitabl  14102  invrfvald  14107  unitlinv  14111  unitrinv  14112  dvrfvald  14118  rdivmuldivd  14129  invrpropdg  14134  dfrhm2  14139  rhmex  14142  rhmunitinv  14163  isnzr2  14169  issubrng  14184  issubrg  14206  subrgugrp  14225  rrgval  14247  isdomn  14254  aprval  14267  aprap  14271  islmod  14276  scaffvalg  14291  rmodislmod  14336  lssex  14339  lsssetm  14341  islssm  14342  islssmg  14343  islss3  14364  lspfval  14373  lspval  14375  lspcl  14376  lspex  14380  sraval  14422  sralemg  14423  srascag  14427  sravscag  14428  sraipg  14429  sraex  14431  qusrhm  14513  psrval  14651  fnpsr  14652  psrbasg  14659  psrelbas  14660  psrplusgg  14663  psraddcl  14665  psr0cl  14666  psrnegcl  14668  psr1clfi  14673  mplvalcoe  14675  fnmpl  14678  mplplusgg  14688  vtxvalg  15838  vtxex  15840