![]() |
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 4976 | . 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦) | |
2 | funfveu 5262 | . . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ∃!𝑦 𝐴𝐹𝑦) | |
3 | euiotaex 4949 | . . 3 ⊢ (∃!𝑦 𝐴𝐹𝑦 → (℩𝑦𝐴𝐹𝑦) ∈ V) | |
4 | 2, 3 | syl 14 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ V) |
5 | 1, 4 | syl5eqel 2169 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∈ wcel 1434 ∃!weu 1943 Vcvv 2612 class class class wbr 3811 dom cdm 4400 ℩cio 4931 Fun wfun 4962 ‘cfv 4968 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3922 ax-pow 3974 ax-pr 3999 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-v 2614 df-sbc 2827 df-un 2988 df-in 2990 df-ss 2997 df-pw 3408 df-sn 3428 df-pr 3429 df-op 3431 df-uni 3628 df-br 3812 df-opab 3866 df-id 4083 df-cnv 4408 df-co 4409 df-dm 4410 df-iota 4933 df-fun 4970 df-fv 4976 |
This theorem is referenced by: fnbrfvb 5289 fvelrnb 5296 funimass4 5299 fvelimab 5304 fniinfv 5306 funfvdm 5311 dmfco 5316 fvco2 5317 eqfnfv 5341 fndmdif 5348 fndmin 5350 fvimacnvi 5357 fvimacnv 5358 funconstss 5361 fniniseg 5363 fniniseg2 5365 fnniniseg2 5366 rexsupp 5367 fvelrn 5374 rexrn 5380 ralrn 5381 dff3im 5388 fmptco 5405 fsn2 5412 fnressn 5424 resfunexg 5457 eufnfv 5464 funfvima3 5467 rexima 5473 ralima 5474 fniunfv 5480 elunirn 5484 dff13 5486 foeqcnvco 5508 f1eqcocnv 5509 isocnv2 5530 isoini 5535 f1oiso 5543 fnovex 5616 suppssof1 5806 offveqb 5808 1stexg 5872 2ndexg 5873 smoiso 5998 rdgtfr 6070 rdgruledefgg 6071 rdgivallem 6077 frectfr 6096 frecrdg 6104 en1 6445 fundmen 6452 fnfi 6570 ordiso2 6634 climshft2 10518 |
Copyright terms: Public domain | W3C validator |