Theorem basfn 13358

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

Syntax hints:  Vcvv 2815   Fn wfn 5352  Basecbs 13299

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 2207  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-int 3955  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-iota 5317  df-fun 5359  df-fn 5360  df-fv 5365  df-inn 9258  df-ndx 13302  df-slot 13303  df-base 13305

This theorem is referenced by:  basmex  13359  basmexd  13360  ressbas2d  13368  ressbasid  13370  strressid  13371  ressval3d  13372  imasex  13572  imasival  13573  imasbas  13574  imasplusg  13575  imasmulr  13576  imasaddfn  13584  imasaddval  13585  imasaddf  13586  imasmulfn  13587  imasmulval  13588  imasmulf  13589  qusval  13590  qusex  13592  qusaddvallemg  13600  qusaddflemg  13601  qusaddval  13602  qusaddf  13603  qusmulval  13604  qusmulf  13605  ismgm  13623  ismgmn0  13624  plusffvalg  13628  grpidvalg  13639  fn0g  13641  gsumress  13661  issgrp  13669  ismnddef  13682  issubmnd  13706  ress0g  13707  ismhm  13719  mhmex  13720  issubm  13730  grppropstrg  13777  grpinvfvalg  13800  grpinvval  13801  grpinvfng  13802  grpsubfvalg  13803  grpsubval  13804  grpressid  13819  grplactfval  13859  qusgrp2  13869  mulgfvalg  13877  mulgval  13878  mulgex  13879  mulgfng  13880  issubg  13929  subgex  13932  issubg2m  13945  isnsg  13958  releqgg  13976  eqgex  13977  eqgfval  13978  eqgen  13983  isghm  13999  ablressid  14091  prdsex  14117  prdsval  14118  prdsbaslemss  14119  prdsbas  14121  prdsplusg  14122  prdsmulr  14123  xpsval  14146  pwsbas  14150  pwselbasb  14151  pwssnf1o  14156  isrng  14176  rngressid  14196  qusrng  14200  issrg  14211  isring  14246  ringidss  14275  ringressid  14309  qusring2  14312  dvdsrvald  14341  dvdsrex  14346  unitgrp  14364  unitabl  14365  invrfvald  14370  unitlinv  14374  unitrinv  14375  dvrfvald  14381  rdivmuldivd  14392  invrpropdg  14397  dfrhm2  14402  rhmex  14405  rhmunitinv  14426  isnzr2  14432  issubrng  14448  issubrg  14470  subrgugrp  14489  rrgval  14511  isdomn  14519  aprval  14532  aprap  14539  aprprop  14542  islmod  14568  scaffvalg  14583  rmodislmod  14628  lssex  14631  lsssetm  14633  islssm  14634  islssmg  14635  islss3  14656  lspfval  14665  lspval  14667  lspcl  14668  lspex  14672  sraval  14714  sralemg  14715  srascag  14719  sravscag  14720  sraipg  14721  sraex  14723  qusrhm  14805  psrval  14943  fnpsr  14944  psrbasg  14958  psrelbas  14959  psrplusgg  14962  psraddcl  14964  psr0cl  14965  psrnegcl  14967  psr1clfi  14972  mplvalcoe  14974  fnmpl  14977  mplplusgg  14987  vtxvalg  16140  vtxex  16142