Theorem basfn 13389

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

Syntax hints:   _Vcvv 2821   Fn wfn 5367   Basecbs 13330

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 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 4244  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-cnex 8260  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266

This theorem 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 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-int 3966  df-br 4126  df-opab 4188  df-mpt 4189  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-iota 5332  df-fun 5374  df-fn 5375  df-fv 5380  df-inn 9284  df-ndx 13333  df-slot 13334  df-base 13336

This theorem is referenced by:  basmex  13390  basmexd  13391  ressbas2d  13399  ressbasid  13401  strressid  13402  ressval3d  13403  imasex  13603  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfn  13615  imasaddval  13616  imasaddf  13617  imasmulfn  13618  imasmulval  13619  imasmulf  13620  qusval  13621  qusex  13623  qusaddvallemg  13631  qusaddflemg  13632  qusaddval  13633  qusaddf  13634  qusmulval  13635  qusmulf  13636  ismgm  13654  ismgmn0  13655  plusffvalg  13659  grpidvalg  13670  fn0g  13672  gzsumress  13689  issgrp  13695  ismnddef  13708  issubmnd  13732  ress0g  13733  ismhm  13745  mhmex  13746  issubm  13756  grppropstrg  13801  grpinvfvalg  13824  grpinvval  13825  grpinvfng  13826  grpsubfvalg  13827  grpsubval  13828  grpressid  13843  grplactfval  13883  qusgrp2  13893  mulgfvalg  13901  mulgval  13902  mulgex  13903  mulgfng  13904  issubg  13953  subgex  13956  issubg2m  13969  isnsg  13982  releqgg  14000  eqgex  14001  eqgfval  14002  eqgen  14007  isghm  14023  ablressid  14116  prdsex  14149  prdsval  14150  prdsbaslemss  14151  prdsbas  14153  prdsplusg  14154  prdsmulr  14155  xpsval  14178  pwsbas  14182  pwselbasb  14183  pwssnf1o  14188  isrng  14208  rngressid  14228  qusrng  14232  issrg  14243  isring  14278  ringidss  14307  ringressid  14341  qusring2  14344  dvdsrvald  14373  dvdsrex  14378  unitgrp  14396  unitabl  14397  invrfvald  14402  unitlinv  14406  unitrinv  14407  dvrfvald  14413  rdivmuldivd  14424  invrpropdg  14429  dfrhm2  14434  rhmex  14437  rhmunitinv  14458  isnzr2  14464  issubrng  14480  issubrg  14502  subrgugrp  14521  rrgval  14543  isdomn  14551  aprval  14564  aprap  14571  aprprop  14574  islmod  14600  scaffvalg  14615  rmodislmod  14660  lssex  14663  lsssetm  14665  islssm  14666  islssmg  14667  islss3  14688  lspfval  14697  lspval  14699  lspcl  14700  lspex  14704  sraval  14746  sralemg  14747  srascag  14751  sravscag  14752  sraipg  14753  sraex  14755  qusrhm  14837  psrval  14973  fnpsr  14974  psrbasg  14988  psrelbas  14989  psrplusgg  14992  psraddcl  14994  psr0cl  14995  psrnegcl  14997  psr1clfi  15002  mplvalcoe  15004  fnmpl  15007  mplplusgg  15017  vtxvalg  16171  vtxex  16173