![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ndxarg | Structured version Visualization version Unicode version |
Description: Get the numeric argument from a defined structure component extractor such as df-base 15174. (Contributed by Mario Carneiro, 6-Oct-2013.) |
Ref | Expression |
---|---|
ndxarg.1 |
![]() ![]() ![]() ![]() |
ndxarg.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ndxarg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ndx 15172 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nnex 10642 |
. . . . 5
![]() ![]() ![]() ![]() | |
3 | resiexg 6755 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ax-mp 5 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2535 |
. . 3
![]() ![]() ![]() ![]() |
6 | ndxarg.1 |
. . 3
![]() ![]() ![]() ![]() | |
7 | 5, 6 | strfvn 15186 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1 | fveq1i 5888 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | ndxarg.2 |
. . 3
![]() ![]() ![]() ![]() | |
10 | fvresi 6113 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | ax-mp 5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 7, 8, 11 | 3eqtri 2487 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6609 ax-cnex 9620 ax-resscn 9621 ax-1cn 9622 ax-icn 9623 ax-addcl 9624 ax-addrcl 9625 ax-mulcl 9626 ax-mulrcl 9627 ax-i2m1 9632 ax-1ne0 9633 ax-rrecex 9636 ax-cnre 9637 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-reu 2755 df-rab 2757 df-v 3058 df-sbc 3279 df-csb 3375 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-pss 3431 df-nul 3743 df-if 3893 df-pw 3964 df-sn 3980 df-pr 3982 df-tp 3984 df-op 3986 df-uni 4212 df-iun 4293 df-br 4416 df-opab 4475 df-mpt 4476 df-tr 4511 df-eprel 4763 df-id 4767 df-po 4773 df-so 4774 df-fr 4811 df-we 4813 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-pred 5398 df-ord 5444 df-on 5445 df-lim 5446 df-suc 5447 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-ov 6317 df-om 6719 df-wrecs 7053 df-recs 7115 df-rdg 7153 df-nn 10637 df-ndx 15172 df-slot 15173 |
This theorem is referenced by: ndxid 15190 basendx 15221 basendxnn 15222 resslem 15230 plusgndx 15272 2strstr 15278 2strstr1 15281 2strop1 15283 mulrndx 15290 starvndx 15296 scandx 15305 vscandx 15307 ipndx 15314 tsetndx 15332 plendx 15339 ocndx 15346 dsndx 15348 unifndx 15350 homndx 15360 ccondx 15362 slotsbhcdif 15366 oppglem 17049 mgplem 17776 opprlem 17904 sralem 18448 opsrbaslem 18749 zlmlem 19136 znbaslem 19157 tnglem 21696 itvndx 24536 lngndx 24537 ttglem 24954 cchhllem 24965 resvlem 28642 hlhilslem 35553 edgfndxnn 39142 baseltedgf 39144 basendxnmulrndx 40226 |
Copyright terms: Public domain | W3C validator |