Theorem basfn 12570

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

Syntax hints:   _Vcvv 2752   Fn wfn 5230   Basecbs 12512

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-cnex 7932  ax-resscn 7933  ax-1re 7935  ax-addrcl 7938

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-iota 5196  df-fun 5237  df-fn 5238  df-fv 5243  df-inn 8950  df-ndx 12515  df-slot 12516  df-base 12518

This theorem is referenced by:  basmex  12571  basmexd  12572  ressbas2d  12580  ressbasid  12582  strressid  12583  ressval3d  12584  prdsex  12774  imasex  12782  imasival  12783  imasbas  12784  imasplusg  12785  imasmulr  12786  imasaddfn  12794  imasaddval  12795  imasaddf  12796  imasmulfn  12797  imasmulval  12798  imasmulf  12799  qusval  12800  qusex  12802  qusaddvallemg  12809  qusaddflemg  12810  qusaddval  12811  qusaddf  12812  qusmulval  12813  qusmulf  12814  xpsval  12828  ismgm  12833  ismgmn0  12834  plusffvalg  12838  grpidvalg  12849  fn0g  12851  issgrp  12866  ismnddef  12879  issubmnd  12903  ress0g  12904  ismhm  12913  mhmex  12914  issubm  12924  grppropstrg  12964  grpinvfvalg  12986  grpinvval  12987  grpinvfng  12988  grpsubfvalg  12989  grpsubval  12990  grpressid  13005  grplactfval  13045  qusgrp2  13055  mulgfvalg  13063  mulgval  13064  mulgex  13065  mulgfng  13066  issubg  13112  subgex  13115  issubg2m  13128  isnsg  13141  releqgg  13159  eqgex  13160  eqgfval  13161  eqgen  13166  isghm  13182  ablressid  13272  isrng  13288  rngressid  13308  qusrng  13312  issrg  13319  isring  13354  ringidss  13383  ringressid  13413  qusring2  13416  reldvdsrsrg  13442  dvdsrvald  13443  dvdsrex  13448  unitgrp  13466  unitabl  13467  invrfvald  13472  unitlinv  13476  unitrinv  13477  dvrfvald  13483  rdivmuldivd  13494  invrpropdg  13499  dfrhm2  13504  rhmex  13507  rhmunitinv  13528  issubrng  13546  issubrg  13568  subrgugrp  13587  aprval  13598  aprap  13602  islmod  13607  scaffvalg  13622  rmodislmod  13667  lssex  13670  lsssetm  13672  islssm  13673  islssmg  13674  islss3  13695  lspfval  13704  lspval  13706  lspcl  13707  lspex  13711  sraval  13753  sralemg  13754  srascag  13758  sravscag  13759  sraipg  13760  sraex  13762  psrval  13944  fnpsr  13945  psrbasg  13951  psrelbas  13952