![]() |
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 2113 |
. 2
![]() ![]() ![]() ![]() | |
2 | fvmptg.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eqeq2d 2124 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eqeq1 2119 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | moeq 2826 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | fvmptg.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | df-mpt 3949 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | eqtri 2133 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 3, 4, 6, 9 | fvopab3ig 5447 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 1, 10 | mpi 15 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-14 1473 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-sep 4004 ax-pow 4056 ax-pr 4089 |
This theorem depends on definitions: df-bi 116 df-3an 945 df-tru 1315 df-nf 1418 df-sb 1717 df-eu 1976 df-mo 1977 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-ral 2393 df-rex 2394 df-v 2657 df-sbc 2877 df-un 3039 df-in 3041 df-ss 3048 df-pw 3476 df-sn 3497 df-pr 3498 df-op 3500 df-uni 3701 df-br 3894 df-opab 3948 df-mpt 3949 df-id 4173 df-xp 4503 df-rel 4504 df-cnv 4505 df-co 4506 df-dm 4507 df-iota 5044 df-fun 5081 df-fv 5087 |
This theorem is referenced by: fvmpt 5450 fvmpts 5451 fvmpt3 5452 fvmpt2 5456 f1mpt 5624 caofinvl 5956 1stvalg 5992 2ndvalg 5993 brtpos2 6100 rdgon 6235 frec0g 6246 freccllem 6251 frecfcllem 6253 frecsuclem 6255 sucinc 6293 sucinc2 6294 omcl 6309 oeicl 6310 oav2 6311 omv2 6313 fvdiagfn 6539 djulclr 6884 djurclr 6885 djulcl 6886 djurcl 6887 djulclb 6890 omp1eomlem 6929 ctmlemr 6943 nnnninf 6971 cardval3ex 6988 ceilqval 9966 frec2uzzd 10060 frec2uzsucd 10061 monoord2 10137 iseqf1olemqval 10147 iseqf1olemqk 10154 seq3f1olemqsum 10160 seq3f1oleml 10163 seq3f1o 10164 seq3distr 10173 ser3le 10178 hashinfom 10411 hashennn 10413 cjval 10504 reval 10508 imval 10509 cvg1nlemcau 10642 cvg1nlemres 10643 absval 10659 resqrexlemglsq 10680 resqrexlemga 10681 climmpt 10955 climle 10989 climcvg1nlem 11004 summodclem3 11035 summodclem2a 11036 zsumdc 11039 fsum3 11042 fsumcl2lem 11053 sumsnf 11064 isumadd 11086 fsumrev 11098 fsumshft 11099 fsummulc2 11103 iserabs 11130 isumlessdc 11151 divcnv 11152 trireciplem 11155 trirecip 11156 expcnvap0 11157 expcnvre 11158 expcnv 11159 explecnv 11160 geolim 11166 geolim2 11167 geo2lim 11171 geoisum 11172 geoisumr 11173 geoisum1 11174 geoisum1c 11175 cvgratz 11187 mertenslem2 11191 mertensabs 11192 eftvalcn 11208 efval 11212 efcvgfsum 11218 ege2le3 11222 efcj 11224 eftlub 11241 efgt1p2 11246 eflegeo 11253 sinval 11254 cosval 11255 tanvalap 11260 eirraplem 11325 phival 11728 crth 11739 phimullem 11740 ennnfonelemj0 11753 ennnfonelem0 11757 strnfvnd 11816 topnvalg 11969 toponsspwpwg 12026 tgval 12055 cldval 12105 ntrfval 12106 clsfval 12107 neifval 12146 neival 12149 ismet 12327 isxmet 12328 divcnap 12535 mulc1cncf 12556 djucllem 12690 nnsf 12880 peano3nninf 12882 nninfalllemn 12883 nninfself 12890 nninfsellemeqinf 12893 |
Copyright terms: Public domain | W3C validator |