Theorem basfn 12520

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

Syntax hints:  Vcvv 2738   Fn wfn 5212  Basecbs 12462

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-sbc 2964  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-iota 5179  df-fun 5219  df-fn 5220  df-fv 5225  df-inn 8920  df-ndx 12465  df-slot 12466  df-base 12468

This theorem is referenced by:  basmex  12521  basmexd  12522  ressbas2d  12528  strressid  12530  ressval3d  12531  prdsex  12718  imasex  12726  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  imasaddfn  12738  imasaddval  12739  imasaddf  12740  imasmulfn  12741  imasmulval  12742  imasmulf  12743  qusval  12744  qusaddvallemg  12752  qusaddflemg  12753  qusaddval  12754  qusaddf  12755  qusmulval  12756  qusmulf  12757  xpsval  12771  ismgm  12776  ismgmn0  12777  plusffvalg  12781  grpidvalg  12792  fn0g  12794  issgrp  12809  ismnddef  12819  issubmnd  12843  ress0g  12844  ismhm  12853  issubm  12863  grppropstrg  12895  grpinvfvalg  12915  grpinvval  12916  grpinvfng  12917  grpsubfvalg  12918  grpsubval  12919  grpressid  12931  grplactfval  12971  mulgfvalg  12985  mulgval  12986  mulgfng  12987  issubg  13033  subgex  13036  issubg2m  13049  isnsg  13062  releqgg  13080  eqgfval  13081  eqgen  13086  issrg  13148  isring  13183  ringidss  13212  ringressid  13238  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrex  13267  unitgrp  13285  unitabl  13286  invrfvald  13291  unitlinv  13295  unitrinv  13296  dvrfvald  13302  rdivmuldivd  13313  invrpropdg  13318  issubrg  13342  subrgugrp  13361  aprval  13372  aprap  13376  islmod  13381  scaffvalg  13396  rmodislmod  13441