Theorem baseid 17139

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

Syntax hints:   = wceq 1541  ‘cfv 6492  1c1 11027  Slot cslot 17108  ndxcnx 17120  Basecbs 17136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  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 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-slot 17109  df-ndx 17121  df-base 17137

This theorem is referenced by:  basfn  17140  base0  17141  basndxelwund  17147  opelstrbas  17149  1strbas  17151  2strbas  17155  ressbas  17163  ressval3d  17173  wunress  17176  rngbase  17219  srngbase  17230  lmodbase  17246  ipsbase  17257  phlbase  17267  topgrpbas  17282  otpsbas  17297  odrngbas  17324  prdsval  17375  prdsbas  17377  imasbas  17433  oppcbas  17641  rescbas  17753  rescabs  17757  wunfunc  17825  wunnat  17883  fucbas  17887  setcbas  18002  catcbas  18025  catcbaselcl  18038  catcfuccl  18042  estrcbas  18048  estrcbasbas  18054  estrreslem1  18060  catcxpccl  18130  odubas  18214  ipobas  18454  grpss  18884  oppgbas  19280  mgpbas  20080  opprbas  20279  ringcbasbas  20606  rmodislmod  20881  srabase  21129  rlmscaf  21159  islidl  21170  lidlrsppropd  21199  rspsn  21288  cnfldbas  21313  cnfldbasOLD  21328  zlmbas  21472  znbas2  21494  thlbas  21651  psrbas  21889  opsrbas  22005  ply1tmcl  22214  ply1scltm  22223  ply1sclf  22227  ply1scl0OLD  22233  ply1scl1OLD  22236  matbas  22357  tuslem  24210  setsmsbas  24419  tngbas  24585  nrgtrg  24634  trkgbas  28517  ttgbas  28949  setsvtx  29108  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  resvbas  33415  idlsrgbas  33585  bj-endbase  37517  hlhilsbase  42195  opprmndb  42762  opprgrpb  42763  opprablb  42764  algbase  43412  mnringbased  44452  cznrnglem  48501  cznabel  48502  rngcbasALTV  48508  ringcbasALTV  48542  ringcbasbasALTV  48554  catbas  49467  prstcbas  49795  mndtcbasval  49821