![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fndmd | Structured version Visualization version GIF version |
Description: The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Ref | Expression |
---|---|
fndmd.1 | ⊢ (𝜑 → 𝐹 Fn 𝐴) |
Ref | Expression |
---|---|
fndmd | ⊢ (𝜑 → dom 𝐹 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fndmd.1 | . 2 ⊢ (𝜑 → 𝐹 Fn 𝐴) | |
2 | fndm 6425 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → dom 𝐹 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 dom cdm 5519 Fn wfn 6319 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 df-an 400 df-fn 6327 |
This theorem is referenced by: fdm 6495 f1dm 6553 f1o00 6624 fvelimad 6707 f1eqcocnv 7035 offval 7396 ofrfval 7397 fndmexd 7597 dmmpoga 7753 fnwelem 7808 wfrlem17 7954 tfrlem5 7999 ixpiunwdom 9038 dfac12lem1 9554 ackbij2lem3 9652 itunisuc 9830 ttukeylem3 9922 prdsbas2 16734 prdsplusgval 16738 prdsmulrval 16740 prdsleval 16742 prdsvscaval 16744 imasleval 16806 ssclem 17081 isssc 17082 rescval2 17090 issubc2 17098 cofuval 17144 resfval2 17155 resf1st 17156 resf2nd 17157 prdsmgp 19356 lspextmo 19821 dsmmfi 20427 ofco2 21056 neiss2 21706 txdis1cn 22240 qtopcld 22318 qtoprest 22322 kqsat 22336 kqdisj 22337 isr0 22342 elfm3 22555 ovolunlem1 24101 ofpreima 30428 ofpreima2 30429 fnpreimac 30434 fsuppcurry1 30487 fsuppcurry2 30488 pfxf1 30644 s2rn 30646 s3rn 30648 cycpmfvlem 30804 cycpmfv1 30805 cycpmfv2 30806 cycpmfv3 30807 ofcfval 31467 probfinmeasb 31796 bnj564 32125 bnj1121 32367 bnj1442 32431 bnj1450 32432 bnj1501 32449 fnrelpredd 32472 frrlem4 33239 frrlem8 33243 frrlem10 33245 fpr2 33253 frr2 33258 sdclem2 35180 prdstotbnd 35232 diadm 38331 dibdiadm 38451 dibdmN 38453 dicdmN 38480 dihdm 38565 fnchoice 41658 wessf1ornlem 41811 limsupequzlem 42364 climrescn 42390 icccncfext 42529 stoweidlem35 42677 stoweidlem59 42701 smflimmpt 43441 smflimsuplem7 43457 |
Copyright terms: Public domain | W3C validator |