Theorem baseid 17262

Description: Utility theorem: index-independent form of df-base 17260. (Contributed by NM, 20-Oct-2012.)

Assertion

Ref	Expression
baseid	⊢ Base = Slot (Base‘ndx)

Proof of Theorem baseid

Step	Hyp	Ref	Expression
1		df-base 17260	. 2 ⊢ Base = Slot 1
2		1nn 12235	. 2 ⊢ 1 ∈ ℕ
3	1, 2	ndxid 17247	1 ⊢ Base = Slot (Base‘ndx)

Syntax hints:   = wceq 1563  ‘cfv 6525  1c1 11089  Slot cslot 17231  ndxcnx 17243  Basecbs 17259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-1cn 11146  ax-addcl 11148

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-nn 12225  df-slot 17232  df-ndx 17244  df-base 17260

This theorem is referenced by:  basfn  17263  base0  17264  basndxelwund  17270  opelstrbas  17272  1strbas  17274  2strbas  17278  ressbas  17286  ressval3d  17296  wunress  17299  rngbase  17342  srngbase  17353  lmodbase  17369  ipsbase  17380  phlbase  17390  topgrpbas  17405  otpsbas  17420  odrngbas  17447  prdsval  17498  prdsbas  17500  imasbas  17556  oppcbas  17764  rescbas  17876  rescabs  17880  wunfunc  17948  wunnat  18006  fucbas  18010  setcbas  18125  catcbas  18148  catcbaselcl  18161  catcfuccl  18165  estrcbas  18171  estrcbasbas  18177  estrreslem1  18183  catcxpccl  18253  odubas  18337  ipobas  18577  grpss  19011  oppgbas  19412  mgpbas  20212  opprbas  20416  ringcbasbas  20749  rmodislmod  21020  srabase  21267  rlmscaf  21297  islidl  21309  lidlrsppropd  21343  rspsn  21461  cnfldbas  21486  zlmbas  21627  znbas2  21649  thlbas  21806  psrbas  22044  opsrbas  22161  ply1tmcl  22393  ply1scltm  22402  ply1sclf  22406  matbas  22531  tuslem  24384  setsmsbas  24593  tngbas  24759  nrgtrg  24808  trkgbas  28672  ttgbas  29135  setsvtx  29294  rlocbas  33501  rlocaddval  33502  rlocmulval  33503  resvbas  33569  idlsrgbas  33711  bj-endbase  37820  hlhilsbase  42575  opprmndb  43145  opprgrpb  43146  opprablb  43147  algbase  43763  mnringbased  44803  cznrnglem  48879  cznabel  48880  rngcbasALTV  48886  ringcbasALTV  48920  ringcbasbasALTV  48932  catbas  49855  prstcbas  50183  mndtcbasval  50209