Theorem plusgid 17066

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

Assertion

Ref	Expression
plusgid	⊢ +g = Slot (+g‘ndx)

Proof of Theorem plusgid

Step	Hyp	Ref	Expression
1		df-plusg 17052	. 2 ⊢ +g = Slot 2
2		2nn 12126	. 2 ⊢ 2 ∈ ℕ
3	1, 2	ndxid 16975	1 ⊢ +g = Slot (+g‘ndx)

Syntax hints:   = wceq 1540  ‘cfv 6466  2c2 12108  Slot cslot 16959  ndxcnx 16971  +_gcplusg 17039

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-1cn 11009  ax-addcl 11011

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-ov 7320  df-om 7760  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-nn 12054  df-2 12116  df-slot 16960  df-ndx 16972  df-plusg 17052

This theorem is referenced by:  grpplusg  17075  ressplusg  17077  rngplusg  17087  srngplusg  17098  lmodplusg  17114  ipsaddg  17125  phlplusg  17135  topgrpplusg  17150  odrngplusg  17192  prdsplusg  17246  imasplusg  17305  frmdplusg  18569  efmndplusg  18595  grpss  18673  oppgplusfval  19028  mgpplusg  19799  oppradd  19946  rmodislmod  20274  rmodislmodOLD  20275  sraaddg  20526  cnfldadd  20685  zlmplusg  20805  znadd  20829  psrplusg  21233  opsrplusg  21337  ply1plusgfvi  21496  matplusg  21644  tngplusg  23883  ttgplusg  27378  resvplusg  31672  idlsrgplusg  31789  bj-endcomp  35560  hlhilsplus  40177  algaddg  41221  mendplusgfval  41227  mnringaddgd  42069  cznabel  45777  cznrng  45778