![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fdmi | Structured version Visualization version GIF version |
Description: The domain of a mapping. (Contributed by NM, 28-Jul-2008.) |
Ref | Expression |
---|---|
fdmi.1 | ⊢ 𝐹:𝐴⟶𝐵 |
Ref | Expression |
---|---|
fdmi | ⊢ dom 𝐹 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdmi.1 | . 2 ⊢ 𝐹:𝐴⟶𝐵 | |
2 | fdm 6200 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐹 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1620 dom cdm 5254 ⟶wf 6033 |
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 197 df-an 385 df-fn 6040 df-f 6041 |
This theorem is referenced by: f0cli 6521 rankvaln 8823 isnum2 8932 r0weon 8996 cfub 9234 cardcf 9237 cflecard 9238 cfle 9239 cflim2 9248 cfidm 9260 cardf 9535 smobeth 9571 inar1 9760 addcompq 9935 addcomnq 9936 mulcompq 9937 mulcomnq 9938 adderpq 9941 mulerpq 9942 addassnq 9943 mulassnq 9944 distrnq 9946 recmulnq 9949 recclnq 9951 dmrecnq 9953 lterpq 9955 ltanq 9956 ltmnq 9957 ltexnq 9960 nsmallnq 9962 ltbtwnnq 9963 prlem934 10018 ltaddpr 10019 ltexprlem2 10022 ltexprlem3 10023 ltexprlem4 10024 ltexprlem6 10026 ltexprlem7 10027 prlem936 10032 eluzel2 11855 uzssz 11870 elixx3g 12352 ndmioo 12366 elfz2 12497 fz0 12520 elfzoel1 12633 elfzoel2 12634 fzoval 12636 ltweuz 12925 fzofi 12938 dmhashres 13294 s1dm 13550 s2dm 13806 sumz 14623 sumss 14625 prod1 14844 prodss 14847 znnen 15111 unbenlem 15785 prmreclem6 15798 eldmcoa 16887 efgsdm 18314 efgsval 18315 efgsp1 18321 efgsfo 18323 efgredleme 18327 efgred 18332 gexex 18427 torsubg 18428 dmdprd 18568 dprdval 18573 iocpnfordt 21192 icomnfordt 21193 uzrest 21873 qtopbaslem 22734 retopbas 22736 tgqioo 22775 re2ndc 22776 bndth 22929 tchcph 23207 ovolficcss 23409 ismbl 23465 uniiccdif 23517 dyadmbllem 23538 opnmbllem 23540 opnmblALT 23542 mbfimaopnlem 23592 itg1addlem4 23636 dvcmul 23877 dvcmulf 23878 dvexp 23886 c1liplem1 23929 deg1n0ima 24019 pserulm 24346 psercn2 24347 psercnlem2 24348 psercnlem1 24349 psercn 24350 pserdvlem1 24351 pserdvlem2 24352 pserdv 24353 pserdv2 24354 abelth 24365 efcn 24367 efcvx 24373 eff1olem 24464 dvrelog 24553 logf1o2 24566 dvlog 24567 efopn 24574 logtayl 24576 cxpcn3lem 24658 cxpcn3 24659 resqrtcn 24660 atancl 24778 atanval 24781 dvatan 24832 atancn 24833 topnfbey 27607 cnaddabloOLD 27716 cnidOLD 27717 cncvcOLD 27718 cnnv 27812 cnnvba 27814 cncph 27954 dfhnorm2 28259 hilablo 28297 hilid 28298 hilvc 28299 hhnv 28302 hhba 28304 hhph 28315 issh2 28346 hhssabloi 28399 hhssnv 28401 hhshsslem1 28404 imaelshi 29197 rnelshi 29198 nlelshi 29199 xrofsup 29813 coinfliprv 30824 erdszelem2 31452 erdszelem5 31455 erdszelem8 31458 msrrcl 31718 mthmsta 31753 bdaydm 32167 icoreunrn 33489 icoreelrn 33491 relowlpssretop 33494 poimirlem26 33717 poimirlem27 33718 opnmbllem0 33727 dvtan 33742 seff 38979 sblpnf 38980 dvsconst 39000 dvsid 39001 dvsef 39002 expgrowth 39005 binomcxplemdvbinom 39023 binomcxplemdvsum 39025 binomcxplemnotnn0 39026 addcomgi 39131 dmuz 39908 dmico 40264 dvsinax 40599 fvvolioof 40678 fvvolicof 40680 dirkercncflem2 40793 fourierdlem42 40838 hoicvr 41237 ovolval3 41336 |
Copyright terms: Public domain | W3C validator |