Theorem basfn 12934

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

Syntax hints:  Vcvv 2773   Fn wfn 5271  Basecbs 12876

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-pr 4257  ax-un 4484  ax-cnex 8023  ax-resscn 8024  ax-1re 8026  ax-addrcl 8029

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3000  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-int 3888  df-br 4048  df-opab 4110  df-mpt 4111  df-id 4344  df-xp 4685  df-rel 4686  df-cnv 4687  df-co 4688  df-dm 4689  df-rn 4690  df-res 4691  df-iota 5237  df-fun 5278  df-fn 5279  df-fv 5284  df-inn 9044  df-ndx 12879  df-slot 12880  df-base 12882

This theorem is referenced by:  basmex  12935  basmexd  12936  ressbas2d  12944  ressbasid  12946  strressid  12947  ressval3d  12948  prdsex  13145  prdsval  13149  prdsbaslemss  13150  prdsbas  13152  prdsplusg  13153  prdsmulr  13154  pwsbas  13168  pwselbasb  13169  pwssnf1o  13174  imasex  13181  imasival  13182  imasbas  13183  imasplusg  13184  imasmulr  13185  imasaddfn  13193  imasaddval  13194  imasaddf  13195  imasmulfn  13196  imasmulval  13197  imasmulf  13198  qusval  13199  qusex  13201  qusaddvallemg  13209  qusaddflemg  13210  qusaddval  13211  qusaddf  13212  qusmulval  13213  qusmulf  13214  xpsval  13228  ismgm  13233  ismgmn0  13234  plusffvalg  13238  grpidvalg  13249  fn0g  13251  gsumress  13271  issgrp  13279  ismnddef  13294  issubmnd  13318  ress0g  13319  ismhm  13337  mhmex  13338  issubm  13348  grppropstrg  13395  grpinvfvalg  13418  grpinvval  13419  grpinvfng  13420  grpsubfvalg  13421  grpsubval  13422  grpressid  13437  grplactfval  13477  qusgrp2  13493  mulgfvalg  13501  mulgval  13502  mulgex  13503  mulgfng  13504  issubg  13553  subgex  13556  issubg2m  13569  isnsg  13582  releqgg  13600  eqgex  13601  eqgfval  13602  eqgen  13607  isghm  13623  ablressid  13715  isrng  13740  rngressid  13760  qusrng  13764  issrg  13771  isring  13806  ringidss  13835  ringressid  13869  qusring2  13872  reldvdsrsrg  13898  dvdsrvald  13899  dvdsrex  13904  unitgrp  13922  unitabl  13923  invrfvald  13928  unitlinv  13932  unitrinv  13933  dvrfvald  13939  rdivmuldivd  13950  invrpropdg  13955  dfrhm2  13960  rhmex  13963  rhmunitinv  13984  isnzr2  13990  issubrng  14005  issubrg  14027  subrgugrp  14046  rrgval  14068  isdomn  14075  aprval  14088  aprap  14092  islmod  14097  scaffvalg  14112  rmodislmod  14157  lssex  14160  lsssetm  14162  islssm  14163  islssmg  14164  islss3  14185  lspfval  14194  lspval  14196  lspcl  14197  lspex  14201  sraval  14243  sralemg  14244  srascag  14248  sravscag  14249  sraipg  14250  sraex  14252  qusrhm  14334  psrval  14472  fnpsr  14473  psrbasg  14480  psrelbas  14481  psrplusgg  14484  psraddcl  14486  psr0cl  14487  psrnegcl  14489  psr1clfi  14494  mplvalcoe  14496  fnmpl  14499  mplplusgg  14509  vtxvalg  15659  vtxex  15661