Theorem basfn 13292

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

Syntax hints:  Vcvv 2815   Fn wfn 5349  Basecbs 13233

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 4230  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-cnex 8223  ax-resscn 8224  ax-1re 8226  ax-addrcl 8229

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 3045  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-int 3952  df-br 4112  df-opab 4174  df-mpt 4175  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-res 4763  df-iota 5314  df-fun 5356  df-fn 5357  df-fv 5362  df-inn 9243  df-ndx 13236  df-slot 13237  df-base 13239

This theorem is referenced by:  basmex  13293  basmexd  13294  ressbas2d  13302  ressbasid  13304  strressid  13305  ressval3d  13306  prdsex  13503  prdsval  13507  prdsbaslemss  13508  prdsbas  13510  prdsplusg  13511  prdsmulr  13512  pwsbas  13526  pwselbasb  13527  pwssnf1o  13532  imasex  13539  imasival  13540  imasbas  13541  imasplusg  13542  imasmulr  13543  imasaddfn  13551  imasaddval  13552  imasaddf  13553  imasmulfn  13554  imasmulval  13555  imasmulf  13556  qusval  13557  qusex  13559  qusaddvallemg  13567  qusaddflemg  13568  qusaddval  13569  qusaddf  13570  qusmulval  13571  qusmulf  13572  xpsval  13586  ismgm  13591  ismgmn0  13592  plusffvalg  13596  grpidvalg  13607  fn0g  13609  gsumress  13629  issgrp  13637  ismnddef  13652  issubmnd  13676  ress0g  13677  ismhm  13695  mhmex  13696  issubm  13706  grppropstrg  13753  grpinvfvalg  13776  grpinvval  13777  grpinvfng  13778  grpsubfvalg  13779  grpsubval  13780  grpressid  13795  grplactfval  13835  qusgrp2  13851  mulgfvalg  13859  mulgval  13860  mulgex  13861  mulgfng  13862  issubg  13911  subgex  13914  issubg2m  13927  isnsg  13940  releqgg  13958  eqgex  13959  eqgfval  13960  eqgen  13965  isghm  13981  ablressid  14073  isrng  14099  rngressid  14119  qusrng  14123  issrg  14130  isring  14165  ringidss  14194  ringressid  14228  qusring2  14231  dvdsrvald  14260  dvdsrex  14265  unitgrp  14283  unitabl  14284  invrfvald  14289  unitlinv  14293  unitrinv  14294  dvrfvald  14300  rdivmuldivd  14311  invrpropdg  14316  dfrhm2  14321  rhmex  14324  rhmunitinv  14345  isnzr2  14351  issubrng  14367  issubrg  14389  subrgugrp  14408  rrgval  14430  isdomn  14438  aprval  14451  aprap  14458  aprprop  14461  islmod  14488  scaffvalg  14503  rmodislmod  14548  lssex  14551  lsssetm  14553  islssm  14554  islssmg  14555  islss3  14576  lspfval  14585  lspval  14587  lspcl  14588  lspex  14592  sraval  14634  sralemg  14635  srascag  14639  sravscag  14640  sraipg  14641  sraex  14643  qusrhm  14725  psrval  14863  fnpsr  14864  psrbasg  14878  psrelbas  14879  psrplusgg  14882  psraddcl  14884  psr0cl  14885  psrnegcl  14887  psr1clfi  14892  mplvalcoe  14894  fnmpl  14897  mplplusgg  14907  vtxvalg  16060  vtxex  16062