![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > baseid | Structured version Visualization version GIF version |
Description: Utility theorem: index-independent form of df-base 16036. (Contributed by NM, 20-Oct-2012.) |
Ref | Expression |
---|---|
baseid | ⊢ Base = Slot (Base‘ndx) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-base 16036 | . 2 ⊢ Base = Slot 1 | |
2 | 1nn 11194 | . 2 ⊢ 1 ∈ ℕ | |
3 | 1, 2 | ndxid 16056 | 1 ⊢ Base = Slot (Base‘ndx) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1620 ‘cfv 6037 1c1 10100 ndxcnx 16027 Slot cslot 16029 Basecbs 16030 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-cnex 10155 ax-resscn 10156 ax-1cn 10157 ax-icn 10158 ax-addcl 10159 ax-addrcl 10160 ax-mulcl 10161 ax-mulrcl 10162 ax-i2m1 10167 ax-1ne0 10168 ax-rrecex 10171 ax-cnre 10172 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-ral 3043 df-rex 3044 df-reu 3045 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-pss 3719 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-we 5215 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-pred 5829 df-ord 5875 df-on 5876 df-lim 5877 df-suc 5878 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-ov 6804 df-om 7219 df-wrecs 7564 df-recs 7625 df-rdg 7663 df-nn 11184 df-ndx 16033 df-slot 16034 df-base 16036 |
This theorem is referenced by: ressbas 16103 opelstrbas 16151 1strbas 16153 2strbas 16157 2strbas1 16160 rngbase 16174 srngbase 16182 lmodbase 16191 ipsbase 16198 phlbase 16208 topgrpbas 16216 otpsbas 16225 otpsbasOLD 16229 odrngbas 16240 prdsval 16288 prdsbas 16290 imasbas 16345 oppcbas 16550 rescbas 16661 rescabs 16665 fucbas 16792 setcbas 16900 catcbas 16919 estrcbas 16937 xpcbas 16990 odubas 17305 ipobas 17327 grpss 17612 rmodislmod 19104 islidl 19384 lidlrsppropd 19403 rspsn 19427 psrbas 19551 cnfldbas 19923 thlbas 20213 matbas 20392 tuslem 22243 setsmsbas 22452 trkgbas 25514 eengbas 26031 setsvtx 26097 algbase 38219 cznrnglem 42432 cznabel 42433 rngcbasALTV 42462 ringcbasALTV 42525 |
Copyright terms: Public domain | W3C validator |