![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > funfvex | GIF 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 | ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fv 5236 | . 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦) | |
2 | funfveu 5540 | . . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ∃!𝑦 𝐴𝐹𝑦) | |
3 | euiotaex 5206 | . . 3 ⊢ (∃!𝑦 𝐴𝐹𝑦 → (℩𝑦𝐴𝐹𝑦) ∈ V) | |
4 | 2, 3 | syl 14 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ V) |
5 | 1, 4 | eqeltrid 2274 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∃!weu 2036 ∈ wcel 2158 Vcvv 2749 class class class wbr 4015 dom cdm 4638 ℩cio 5188 Fun wfun 5222 ‘cfv 5228 |
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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-pow 4186 ax-pr 4221 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-rex 2471 df-v 2751 df-sbc 2975 df-un 3145 df-in 3147 df-ss 3154 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-br 4016 df-opab 4077 df-id 4305 df-cnv 4646 df-co 4647 df-dm 4648 df-iota 5190 df-fun 5230 df-fv 5236 |
This theorem is referenced by: fnbrfvb 5569 fvelrnb 5576 funimass4 5579 fvelimab 5585 fniinfv 5587 funfvdm 5592 dmfco 5597 fvco2 5598 eqfnfv 5626 fndmdif 5634 fndmin 5636 fvimacnvi 5643 fvimacnv 5644 funconstss 5647 fniniseg 5649 fniniseg2 5651 fnniniseg2 5652 rexsupp 5653 fvelrn 5660 rexrn 5666 ralrn 5667 dff3im 5674 fmptco 5695 fsn2 5703 fnressn 5715 resfunexg 5750 eufnfv 5760 funfvima3 5763 rexima 5768 ralima 5769 fniunfv 5776 elunirn 5780 dff13 5782 foeqcnvco 5804 f1eqcocnv 5805 isocnv2 5826 isoini 5832 f1oiso 5840 fnovex 5921 suppssof1 6114 offveqb 6116 1stexg 6182 2ndexg 6183 smoiso 6317 rdgtfr 6389 rdgruledefgg 6390 rdgivallem 6396 frectfr 6415 frecrdg 6423 en1 6813 fundmen 6820 fnfi 6950 ordiso2 7048 cc2lem 7279 climshft2 11328 slotex 12503 strsetsid 12509 ressbas2d 12542 ressbasid 12544 strressid 12545 ressval3d 12546 prdsex 12736 imasex 12744 imasival 12745 imasbas 12746 imasplusg 12747 imasmulr 12748 imasaddfn 12756 imasaddval 12757 imasaddf 12758 imasmulfn 12759 imasmulval 12760 imasmulf 12761 qusval 12762 qusex 12764 qusaddvallemg 12771 qusaddflemg 12772 qusaddval 12773 qusaddf 12774 qusmulval 12775 qusmulf 12776 xpsfeq 12783 xpsval 12790 ismgm 12795 plusffvalg 12800 grpidvalg 12811 fn0g 12813 issgrp 12828 ismnddef 12841 issubmnd 12865 ress0g 12866 ismhm 12875 issubm 12885 0mhm 12895 grppropstrg 12917 grpinvfvalg 12939 grpinvval 12940 grpinvfng 12941 grpsubfvalg 12942 grpsubval 12943 grpressid 12958 grplactfval 12998 qusgrp2 13008 mulgfvalg 13016 mulgval 13017 mulgex 13018 mulgfng 13019 issubg 13065 subgex 13068 issubg2m 13081 isnsg 13094 releqgg 13112 eqgex 13113 eqgfval 13114 eqgen 13119 ablressid 13170 mgptopng 13181 isrng 13186 rngressid 13206 qusrng 13210 dfur2g 13214 issrg 13217 isring 13252 ringidss 13281 ringressid 13311 qusring2 13314 reldvdsrsrg 13340 dvdsrvald 13341 dvdsrex 13346 unitgrp 13364 unitabl 13365 invrfvald 13370 unitlinv 13374 unitrinv 13375 dvrfvald 13381 rdivmuldivd 13392 invrpropdg 13397 issubrng 13419 issubrg 13441 subrgugrp 13460 aprval 13471 aprap 13475 islmod 13480 scaffvalg 13495 rmodislmod 13540 lssex 13543 lsssetm 13545 islssm 13546 islssmg 13547 islss3 13568 lspfval 13577 lspval 13579 lspcl 13580 lspex 13584 sraval 13626 sralemg 13627 srascag 13631 sravscag 13632 sraipg 13633 sraex 13635 rlmsubg 13647 rlmvnegg 13654 ixpsnbasval 13655 lidlex 13662 rspex 13663 lidlss 13665 lidlrsppropdg 13684 |
Copyright terms: Public domain | W3C validator |