![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > funfvex | Unicode version |
Description: The value of a function exists. A special case of Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by Jim Kingdon, 29-Dec-2018.) |
Ref | Expression |
---|---|
funfvex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fv 5243 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | funfveu 5547 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | euiotaex 5212 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl 14 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltrid 2276 |
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-id 4311 df-cnv 4652 df-co 4653 df-dm 4654 df-iota 5196 df-fun 5237 df-fv 5243 |
This theorem is referenced by: fnbrfvb 5577 fvelrnb 5584 funimass4 5587 fvelimab 5593 fniinfv 5595 funfvdm 5600 dmfco 5605 fvco2 5606 eqfnfv 5634 fndmdif 5642 fndmin 5644 fvimacnvi 5651 fvimacnv 5652 funconstss 5655 fniniseg 5657 fniniseg2 5659 fnniniseg2 5660 rexsupp 5661 fvelrn 5668 rexrn 5674 ralrn 5675 dff3im 5682 fmptco 5703 fsn2 5711 fnressn 5723 resfunexg 5758 eufnfv 5768 funfvima3 5771 rexima 5776 ralima 5777 fniunfv 5784 elunirn 5788 dff13 5790 foeqcnvco 5812 f1eqcocnv 5813 isocnv2 5834 isoini 5840 f1oiso 5848 fnovex 5930 suppssof1 6125 offveqb 6127 1stexg 6193 2ndexg 6194 smoiso 6328 rdgtfr 6400 rdgruledefgg 6401 rdgivallem 6407 frectfr 6426 frecrdg 6434 en1 6826 fundmen 6833 fnfi 6967 ordiso2 7065 cc2lem 7296 climshft2 11349 slotex 12542 strsetsid 12548 ressbas2d 12583 ressbasid 12585 strressid 12586 ressval3d 12587 prdsex 12777 imasex 12785 imasival 12786 imasbas 12787 imasplusg 12788 imasmulr 12789 imasaddfn 12797 imasaddval 12798 imasaddf 12799 imasmulfn 12800 imasmulval 12801 imasmulf 12802 qusval 12803 qusex 12805 qusaddvallemg 12812 qusaddflemg 12813 qusaddval 12814 qusaddf 12815 qusmulval 12816 qusmulf 12817 xpsfeq 12824 xpsval 12831 ismgm 12836 plusffvalg 12841 grpidvalg 12852 fn0g 12854 fngsum 12867 igsumvalx 12868 gsumress 12873 gsum0g 12874 issgrp 12881 ismnddef 12894 issubmnd 12918 ress0g 12919 ismhm 12928 mhmex 12929 issubm 12939 0mhm 12953 grppropstrg 12979 grpinvfvalg 13001 grpinvval 13002 grpinvfng 13003 grpsubfvalg 13004 grpsubval 13005 grpressid 13020 grplactfval 13060 qusgrp2 13070 mulgfvalg 13078 mulgval 13079 mulgex 13080 mulgfng 13081 issubg 13129 subgex 13132 issubg2m 13145 isnsg 13158 releqgg 13176 eqgex 13177 eqgfval 13178 eqgen 13183 isghm 13199 ablressid 13289 mgptopng 13300 isrng 13305 rngressid 13325 qusrng 13329 dfur2g 13333 issrg 13336 isring 13371 ringidss 13400 ringressid 13430 qusring2 13433 reldvdsrsrg 13459 dvdsrvald 13460 dvdsrex 13465 unitgrp 13483 unitabl 13484 invrfvald 13489 unitlinv 13493 unitrinv 13494 dvrfvald 13500 rdivmuldivd 13511 invrpropdg 13516 dfrhm2 13521 rhmex 13524 rhmunitinv 13545 issubrng 13563 issubrg 13585 subrgugrp 13604 aprval 13615 aprap 13619 islmod 13624 scaffvalg 13639 rmodislmod 13684 lssex 13687 lsssetm 13689 islssm 13690 islssmg 13691 islss3 13712 lspfval 13721 lspval 13723 lspcl 13724 lspex 13728 sraval 13770 sralemg 13771 srascag 13775 sravscag 13776 sraipg 13777 sraex 13779 rlmsubg 13791 rlmvnegg 13798 ixpsnbasval 13799 lidlex 13806 rspex 13807 lidlss 13809 lidlrsppropdg 13828 psrval 13961 fnpsr 13962 psrbasg 13968 psrelbas 13969 psrplusgg 13971 psraddcl 13973 |
Copyright terms: Public domain | W3C validator |