| 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 6671 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → dom 𝐹 = 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 dom cdm 5685 Fn wfn 6556 |
| 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 207 df-an 396 df-fn 6564 |
| This theorem is referenced by: fdm 6745 f1dm 6808 f1o00 6883 fvelimad 6976 rescnvimafod 7093 f1eqcocnv 7321 ofrfvalg 7705 offval 7706 fndmexd 7926 dmmpoga 8098 fnwelem 8156 frrlem4 8314 frrlem8 8318 frrlem10 8320 fpr2 8329 fprresex 8335 wfrlem17OLD 8365 wfr2 8376 tfrlem5 8420 ixpiunwdom 9630 frr2 9800 dfac12lem1 10184 ackbij2lem3 10280 itunisuc 10459 ttukeylem3 10551 prdsbas2 17514 prdsplusgval 17518 prdsmulrval 17520 prdsleval 17522 prdsvscaval 17524 imasleval 17586 ssclem 17863 isssc 17864 rescval2 17872 issubc2 17881 cofuval 17927 resfval2 17938 resf1st 17939 resf2nd 17940 prdsmgp 20148 lspextmo 21055 dsmmfi 21758 ofco2 22457 neiss2 23109 txdis1cn 23643 qtopcld 23721 qtoprest 23725 kqsat 23739 kqdisj 23740 isr0 23745 elfm3 23958 ovolunlem1 25532 ofpreima 32675 ofpreima2 32676 fnpreimac 32681 fsuppcurry1 32736 fsuppcurry2 32737 pfxf1 32926 s2rnOLD 32928 s3rnOLD 32930 cycpmfvlem 33132 cycpmfv1 33133 cycpmfv2 33134 cycpmfv3 33135 1arithidomlem2 33564 1arithidom 33565 ply1annidllem 33744 ofcfval 34099 probfinmeasb 34430 bnj564 34758 bnj1121 34999 bnj1442 35063 bnj1450 35064 bnj1501 35081 fnrelpredd 35103 sdclem2 37749 prdstotbnd 37801 diadm 41037 dibdiadm 41157 dibdmN 41159 dicdmN 41186 dihdm 41271 aks4d1p1p5 42076 aks6d1c6lem2 42172 tfsconcat0b 43359 fnchoice 45034 wessf1ornlem 45190 limsupequzlem 45737 climrescn 45763 icccncfext 45902 stoweidlem35 46050 stoweidlem59 46074 smflimmpt 46825 smflimsuplem7 46841 |
| Copyright terms: Public domain | W3C validator |