Theorem baseid 17173

Description: Utility theorem: index-independent form of df-base 17171. (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 17171	. 2 ⊢ Base = Slot 1
2		1nn 12176	. 2 ⊢ 1 ∈ ℕ
3	1, 2	ndxid 17158	1 ⊢ Base = Slot (Base‘ndx)

Syntax hints:   = wceq 1542  ‘cfv 6492  1c1 11030  Slot cslot 17142  ndxcnx 17154  Basecbs 17170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166  df-slot 17143  df-ndx 17155  df-base 17171

This theorem is referenced by:  basfn  17174  base0  17175  basndxelwund  17181  opelstrbas  17183  1strbas  17185  2strbas  17189  ressbas  17197  ressval3d  17207  wunress  17210  rngbase  17253  srngbase  17264  lmodbase  17280  ipsbase  17291  phlbase  17301  topgrpbas  17316  otpsbas  17331  odrngbas  17358  prdsval  17409  prdsbas  17411  imasbas  17467  oppcbas  17675  rescbas  17787  rescabs  17791  wunfunc  17859  wunnat  17917  fucbas  17921  setcbas  18036  catcbas  18059  catcbaselcl  18072  catcfuccl  18076  estrcbas  18082  estrcbasbas  18088  estrreslem1  18094  catcxpccl  18164  odubas  18248  ipobas  18488  grpss  18921  oppgbas  19317  mgpbas  20117  opprbas  20314  ringcbasbas  20641  rmodislmod  20916  srabase  21164  rlmscaf  21194  islidl  21205  lidlrsppropd  21234  rspsn  21323  cnfldbas  21348  cnfldbasOLD  21363  zlmbas  21507  znbas2  21529  thlbas  21686  psrbas  21923  opsrbas  22038  ply1tmcl  22247  ply1scltm  22256  ply1sclf  22260  matbas  22388  tuslem  24241  setsmsbas  24450  tngbas  24616  nrgtrg  24665  trkgbas  28527  ttgbas  28959  setsvtx  29118  rlocbas  33343  rlocaddval  33344  rlocmulval  33345  resvbas  33409  idlsrgbas  33579  bj-endbase  37646  hlhilsbase  42399  opprmndb  42970  opprgrpb  42971  opprablb  42972  algbase  43620  mnringbased  44660  cznrnglem  48747  cznabel  48748  rngcbasALTV  48754  ringcbasALTV  48788  ringcbasbasALTV  48800  catbas  49713  prstcbas  50041  mndtcbasval  50067