Theorem basfn 13057

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

Syntax hints:  Vcvv 2779   Fn wfn 5289  Basecbs 12998

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-cnex 8058  ax-resscn 8059  ax-1re 8061  ax-addrcl 8064

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-sbc 3009  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-iota 5254  df-fun 5296  df-fn 5297  df-fv 5302  df-inn 9079  df-ndx 13001  df-slot 13002  df-base 13004

This theorem is referenced by:  basmex  13058  basmexd  13059  ressbas2d  13067  ressbasid  13069  strressid  13070  ressval3d  13071  prdsex  13268  prdsval  13272  prdsbaslemss  13273  prdsbas  13275  prdsplusg  13276  prdsmulr  13277  pwsbas  13291  pwselbasb  13292  pwssnf1o  13297  imasex  13304  imasival  13305  imasbas  13306  imasplusg  13307  imasmulr  13308  imasaddfn  13316  imasaddval  13317  imasaddf  13318  imasmulfn  13319  imasmulval  13320  imasmulf  13321  qusval  13322  qusex  13324  qusaddvallemg  13332  qusaddflemg  13333  qusaddval  13334  qusaddf  13335  qusmulval  13336  qusmulf  13337  xpsval  13351  ismgm  13356  ismgmn0  13357  plusffvalg  13361  grpidvalg  13372  fn0g  13374  gsumress  13394  issgrp  13402  ismnddef  13417  issubmnd  13441  ress0g  13442  ismhm  13460  mhmex  13461  issubm  13471  grppropstrg  13518  grpinvfvalg  13541  grpinvval  13542  grpinvfng  13543  grpsubfvalg  13544  grpsubval  13545  grpressid  13560  grplactfval  13600  qusgrp2  13616  mulgfvalg  13624  mulgval  13625  mulgex  13626  mulgfng  13627  issubg  13676  subgex  13679  issubg2m  13692  isnsg  13705  releqgg  13723  eqgex  13724  eqgfval  13725  eqgen  13730  isghm  13746  ablressid  13838  isrng  13863  rngressid  13883  qusrng  13887  issrg  13894  isring  13929  ringidss  13958  ringressid  13992  qusring2  13995  reldvdsrsrg  14021  dvdsrvald  14022  dvdsrex  14027  unitgrp  14045  unitabl  14046  invrfvald  14051  unitlinv  14055  unitrinv  14056  dvrfvald  14062  rdivmuldivd  14073  invrpropdg  14078  dfrhm2  14083  rhmex  14086  rhmunitinv  14107  isnzr2  14113  issubrng  14128  issubrg  14150  subrgugrp  14169  rrgval  14191  isdomn  14198  aprval  14211  aprap  14215  islmod  14220  scaffvalg  14235  rmodislmod  14280  lssex  14283  lsssetm  14285  islssm  14286  islssmg  14287  islss3  14308  lspfval  14317  lspval  14319  lspcl  14320  lspex  14324  sraval  14366  sralemg  14367  srascag  14371  sravscag  14372  sraipg  14373  sraex  14375  qusrhm  14457  psrval  14595  fnpsr  14596  psrbasg  14603  psrelbas  14604  psrplusgg  14607  psraddcl  14609  psr0cl  14610  psrnegcl  14612  psr1clfi  14617  mplvalcoe  14619  fnmpl  14622  mplplusgg  14632  vtxvalg  15782  vtxex  15784