Theorem basfn 13164

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

Syntax hints:  Vcvv 2801   Fn wfn 5323  Basecbs 13105

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-cnex 8128  ax-resscn 8129  ax-1re 8131  ax-addrcl 8134

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-sbc 3031  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-int 3930  df-br 4090  df-opab 4152  df-mpt 4153  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-iota 5288  df-fun 5330  df-fn 5331  df-fv 5336  df-inn 9149  df-ndx 13108  df-slot 13109  df-base 13111

This theorem is referenced by:  basmex  13165  basmexd  13166  ressbas2d  13174  ressbasid  13176  strressid  13177  ressval3d  13178  prdsex  13375  prdsval  13379  prdsbaslemss  13380  prdsbas  13382  prdsplusg  13383  prdsmulr  13384  pwsbas  13398  pwselbasb  13399  pwssnf1o  13404  imasex  13411  imasival  13412  imasbas  13413  imasplusg  13414  imasmulr  13415  imasaddfn  13423  imasaddval  13424  imasaddf  13425  imasmulfn  13426  imasmulval  13427  imasmulf  13428  qusval  13429  qusex  13431  qusaddvallemg  13439  qusaddflemg  13440  qusaddval  13441  qusaddf  13442  qusmulval  13443  qusmulf  13444  xpsval  13458  ismgm  13463  ismgmn0  13464  plusffvalg  13468  grpidvalg  13479  fn0g  13481  gsumress  13501  issgrp  13509  ismnddef  13524  issubmnd  13548  ress0g  13549  ismhm  13567  mhmex  13568  issubm  13578  grppropstrg  13625  grpinvfvalg  13648  grpinvval  13649  grpinvfng  13650  grpsubfvalg  13651  grpsubval  13652  grpressid  13667  grplactfval  13707  qusgrp2  13723  mulgfvalg  13731  mulgval  13732  mulgex  13733  mulgfng  13734  issubg  13783  subgex  13786  issubg2m  13799  isnsg  13812  releqgg  13830  eqgex  13831  eqgfval  13832  eqgen  13837  isghm  13853  ablressid  13945  isrng  13971  rngressid  13991  qusrng  13995  issrg  14002  isring  14037  ringidss  14066  ringressid  14100  qusring2  14103  dvdsrvald  14131  dvdsrex  14136  unitgrp  14154  unitabl  14155  invrfvald  14160  unitlinv  14164  unitrinv  14165  dvrfvald  14171  rdivmuldivd  14182  invrpropdg  14187  dfrhm2  14192  rhmex  14195  rhmunitinv  14216  isnzr2  14222  issubrng  14237  issubrg  14259  subrgugrp  14278  rrgval  14300  isdomn  14307  aprval  14320  aprap  14324  islmod  14329  scaffvalg  14344  rmodislmod  14389  lssex  14392  lsssetm  14394  islssm  14395  islssmg  14396  islss3  14417  lspfval  14426  lspval  14428  lspcl  14429  lspex  14433  sraval  14475  sralemg  14476  srascag  14480  sravscag  14481  sraipg  14482  sraex  14484  qusrhm  14566  psrval  14704  fnpsr  14705  psrbasg  14717  psrelbas  14718  psrplusgg  14721  psraddcl  14723  psr0cl  14724  psrnegcl  14726  psr1clfi  14731  mplvalcoe  14733  fnmpl  14736  mplplusgg  14746  vtxvalg  15896  vtxex  15898