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 5204 | . 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦) | |
2 | funfveu 5507 | . . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ∃!𝑦 𝐴𝐹𝑦) | |
3 | euiotaex 5174 | . . 3 ⊢ (∃!𝑦 𝐴𝐹𝑦 → (℩𝑦𝐴𝐹𝑦) ∈ V) | |
4 | 2, 3 | syl 14 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ V) |
5 | 1, 4 | eqeltrid 2257 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∃!weu 2019 ∈ wcel 2141 Vcvv 2730 class class class wbr 3987 dom cdm 4609 ℩cio 5156 Fun wfun 5190 ‘cfv 5196 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-14 2144 ax-ext 2152 ax-sep 4105 ax-pow 4158 ax-pr 4192 |
This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-v 2732 df-sbc 2956 df-un 3125 df-in 3127 df-ss 3134 df-pw 3566 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-br 3988 df-opab 4049 df-id 4276 df-cnv 4617 df-co 4618 df-dm 4619 df-iota 5158 df-fun 5198 df-fv 5204 |
This theorem is referenced by: fnbrfvb 5535 fvelrnb 5542 funimass4 5545 fvelimab 5550 fniinfv 5552 funfvdm 5557 dmfco 5562 fvco2 5563 eqfnfv 5591 fndmdif 5598 fndmin 5600 fvimacnvi 5607 fvimacnv 5608 funconstss 5611 fniniseg 5613 fniniseg2 5615 fnniniseg2 5616 rexsupp 5617 fvelrn 5624 rexrn 5630 ralrn 5631 dff3im 5638 fmptco 5659 fsn2 5667 fnressn 5679 resfunexg 5714 eufnfv 5723 funfvima3 5726 rexima 5731 ralima 5732 fniunfv 5738 elunirn 5742 dff13 5744 foeqcnvco 5766 f1eqcocnv 5767 isocnv2 5788 isoini 5794 f1oiso 5802 fnovex 5883 suppssof1 6075 offveqb 6077 1stexg 6143 2ndexg 6144 smoiso 6278 rdgtfr 6350 rdgruledefgg 6351 rdgivallem 6357 frectfr 6376 frecrdg 6384 en1 6773 fundmen 6780 fnfi 6910 ordiso2 7008 cc2lem 7215 climshft2 11256 slotex 12430 strsetsid 12436 ismgm 12598 plusffvalg 12603 grpidvalg 12614 fn0g 12616 issgrp 12631 ismnddef 12641 ismhm 12672 issubm 12682 0mhm 12691 |
Copyright terms: Public domain | W3C validator |