![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fvmptg | Unicode version |
Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
fvmptg.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
fvmptg.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fvmptg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2189 |
. 2
![]() ![]() ![]() ![]() | |
2 | fvmptg.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eqeq2d 2201 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eqeq1 2196 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | moeq 2927 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | fvmptg.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | df-mpt 4081 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | eqtri 2210 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 3, 4, 6, 9 | fvopab3ig 5611 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 1, 10 | mpi 15 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4192 ax-pr 4227 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-v 2754 df-sbc 2978 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-br 4019 df-opab 4080 df-mpt 4081 df-id 4311 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-iota 5196 df-fun 5237 df-fv 5243 |
This theorem is referenced by: fvmpt 5614 fvmpts 5615 fvmpt3 5616 fvmpt2 5620 f1mpt 5793 caofinvl 6129 1stvalg 6167 2ndvalg 6168 brtpos2 6276 rdgon 6411 frec0g 6422 freccllem 6427 frecfcllem 6429 frecsuclem 6431 sucinc 6470 sucinc2 6471 omcl 6486 oeicl 6487 oav2 6488 omv2 6490 fvdiagfn 6719 djulclr 7078 djurclr 7079 djulcl 7080 djurcl 7081 djulclb 7084 omp1eomlem 7123 ctmlemr 7137 nnnninf 7154 nnnninfeq 7156 cardval3ex 7214 ceilqval 10337 frec2uzzd 10431 frec2uzsucd 10432 monoord2 10508 iseqf1olemqval 10518 iseqf1olemqk 10525 seq3f1olemqsum 10531 seq3f1oleml 10534 seq3f1o 10535 seq3distr 10544 ser3le 10549 hashinfom 10790 hashennn 10792 cjval 10886 reval 10890 imval 10891 cvg1nlemcau 11025 cvg1nlemres 11026 absval 11042 resqrexlemglsq 11063 resqrexlemga 11064 climmpt 11340 climle 11374 climcvg1nlem 11389 summodclem3 11420 summodclem2a 11421 zsumdc 11424 fsum3 11427 fsumcl2lem 11438 sumsnf 11449 isumadd 11471 fsumrev 11483 fsumshft 11484 fsummulc2 11488 iserabs 11515 isumlessdc 11536 divcnv 11537 trireciplem 11540 trirecip 11541 expcnvap0 11542 expcnvre 11543 expcnv 11544 explecnv 11545 geolim 11551 geolim2 11552 geo2lim 11556 geoisum 11557 geoisumr 11558 geoisum1 11559 geoisum1c 11560 cvgratz 11572 mertenslem2 11576 mertensabs 11577 fprodmul 11631 eftvalcn 11697 efval 11701 efcvgfsum 11707 ege2le3 11711 efcj 11713 eftlub 11730 efgt1p2 11735 eflegeo 11741 sinval 11742 cosval 11743 tanvalap 11748 eirraplem 11816 phival 12245 crth 12256 phimullem 12257 ennnfonelemj0 12452 ennnfonelem0 12456 strnfvnd 12532 topnvalg 12756 tgval 12767 toponsspwpwg 13979 cldval 14056 ntrfval 14057 clsfval 14058 neifval 14097 neival 14100 ismet 14301 isxmet 14302 divcnap 14512 mulc1cncf 14533 djucllem 15010 nnsf 15213 peano3nninf 15215 nninfself 15221 nninfsellemeqinf 15224 dceqnconst 15267 dcapnconst 15268 |
Copyright terms: Public domain | W3C validator |