![]() |
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 2177 |
. 2
![]() ![]() ![]() ![]() | |
2 | fvmptg.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eqeq2d 2189 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eqeq1 2184 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | moeq 2912 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | fvmptg.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | df-mpt 4066 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | eqtri 2198 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 3, 4, 6, 9 | fvopab3ig 5590 |
. 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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-14 2151 ax-ext 2159 ax-sep 4121 ax-pow 4174 ax-pr 4209 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-v 2739 df-sbc 2963 df-un 3133 df-in 3135 df-ss 3142 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-br 4004 df-opab 4065 df-mpt 4066 df-id 4293 df-xp 4632 df-rel 4633 df-cnv 4634 df-co 4635 df-dm 4636 df-iota 5178 df-fun 5218 df-fv 5224 |
This theorem is referenced by: fvmpt 5593 fvmpts 5594 fvmpt3 5595 fvmpt2 5599 f1mpt 5771 caofinvl 6104 1stvalg 6142 2ndvalg 6143 brtpos2 6251 rdgon 6386 frec0g 6397 freccllem 6402 frecfcllem 6404 frecsuclem 6406 sucinc 6445 sucinc2 6446 omcl 6461 oeicl 6462 oav2 6463 omv2 6465 fvdiagfn 6692 djulclr 7047 djurclr 7048 djulcl 7049 djurcl 7050 djulclb 7053 omp1eomlem 7092 ctmlemr 7106 nnnninf 7123 nnnninfeq 7125 cardval3ex 7183 ceilqval 10305 frec2uzzd 10399 frec2uzsucd 10400 monoord2 10476 iseqf1olemqval 10486 iseqf1olemqk 10493 seq3f1olemqsum 10499 seq3f1oleml 10502 seq3f1o 10503 seq3distr 10512 ser3le 10517 hashinfom 10757 hashennn 10759 cjval 10853 reval 10857 imval 10858 cvg1nlemcau 10992 cvg1nlemres 10993 absval 11009 resqrexlemglsq 11030 resqrexlemga 11031 climmpt 11307 climle 11341 climcvg1nlem 11356 summodclem3 11387 summodclem2a 11388 zsumdc 11391 fsum3 11394 fsumcl2lem 11405 sumsnf 11416 isumadd 11438 fsumrev 11450 fsumshft 11451 fsummulc2 11455 iserabs 11482 isumlessdc 11503 divcnv 11504 trireciplem 11507 trirecip 11508 expcnvap0 11509 expcnvre 11510 expcnv 11511 explecnv 11512 geolim 11518 geolim2 11519 geo2lim 11523 geoisum 11524 geoisumr 11525 geoisum1 11526 geoisum1c 11527 cvgratz 11539 mertenslem2 11543 mertensabs 11544 fprodmul 11598 eftvalcn 11664 efval 11668 efcvgfsum 11674 ege2le3 11678 efcj 11680 eftlub 11697 efgt1p2 11702 eflegeo 11708 sinval 11709 cosval 11710 tanvalap 11715 eirraplem 11783 phival 12212 crth 12223 phimullem 12224 ennnfonelemj0 12401 ennnfonelem0 12405 strnfvnd 12481 topnvalg 12699 tgval 12710 toponsspwpwg 13492 cldval 13569 ntrfval 13570 clsfval 13571 neifval 13610 neival 13613 ismet 13814 isxmet 13815 divcnap 14025 mulc1cncf 14046 djucllem 14522 nnsf 14724 peano3nninf 14726 nninfself 14732 nninfsellemeqinf 14735 dceqnconst 14777 dcapnconst 14778 |
Copyright terms: Public domain | W3C validator |