Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fdmi | Structured version Visualization version GIF version |
Description: Inference associated with fdm 6515. 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 6515 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐹 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 dom cdm 5548 ⟶wf 6344 |
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 208 df-an 397 df-fn 6351 df-f 6352 |
This theorem is referenced by: f0cli 6856 rankvaln 9216 isnum2 9362 r0weon 9426 cfub 9659 cardcf 9662 cflecard 9663 cfle 9664 cflim2 9673 cfidm 9685 cardf 9960 smobeth 9996 inar1 10185 addcompq 10360 addcomnq 10361 mulcompq 10362 mulcomnq 10363 adderpq 10366 mulerpq 10367 addassnq 10368 mulassnq 10369 distrnq 10371 recmulnq 10374 recclnq 10376 dmrecnq 10378 lterpq 10380 ltanq 10381 ltmnq 10382 ltexnq 10385 nsmallnq 10387 ltbtwnnq 10388 prlem934 10443 ltaddpr 10444 ltexprlem2 10447 ltexprlem3 10448 ltexprlem4 10449 ltexprlem6 10451 ltexprlem7 10452 prlem936 10457 eluzel2 12236 uzssz 12252 elixx3g 12739 ndmioo 12753 elfz2 12887 fz0 12910 elfzoel1 13024 elfzoel2 13025 fzoval 13027 ltweuz 13317 fzofi 13330 dmhashres 13689 s1dm 13950 s2dm 14240 sumz 15067 sumss 15069 prod1 15286 prodss 15289 znnen 15553 unbenlem 16232 prmreclem6 16245 eldmcoa 17313 efgsdm 18785 efgsval 18786 efgsp1 18792 efgsfo 18794 efgredleme 18798 efgred 18803 gexex 18902 torsubg 18903 dmdprd 19049 dprdval 19054 iocpnfordt 21751 icomnfordt 21752 uzrest 22433 qtopbaslem 23294 retopbas 23296 tgqioo 23335 re2ndc 23336 bndth 23489 tcphcph 23767 ovolficcss 23997 ismbl 24054 uniiccdif 24106 dyadmbllem 24127 opnmbllem 24129 opnmblALT 24131 mbfimaopnlem 24183 itg1addlem4 24227 dvcmul 24468 dvcmulf 24469 dvexp 24477 c1liplem1 24520 deg1n0ima 24610 pserulm 24937 psercn2 24938 psercnlem2 24939 psercnlem1 24940 psercn 24941 pserdvlem1 24942 pserdvlem2 24943 pserdv 24944 pserdv2 24945 abelth 24956 efcn 24958 efcvx 24964 eff1olem 25059 dvrelog 25147 logf1o2 25160 dvlog 25161 efopn 25168 logtayl 25170 cxpcn3lem 25255 cxpcn3 25256 resqrtcn 25257 atancl 25386 atanval 25389 dvatan 25440 atancn 25441 topnfbey 28175 cnaddabloOLD 28285 cnidOLD 28286 cncvcOLD 28287 cnnv 28381 cnnvba 28383 cncph 28523 dfhnorm2 28826 hilablo 28864 hilid 28865 hilvc 28866 hhnv 28869 hhba 28871 hhph 28882 issh2 28913 hhssabloi 28966 hhssnv 28968 hhshsslem1 28971 imaelshi 29762 rnelshi 29763 nlelshi 29764 xrofsup 30418 coinfliprv 31639 erdszelem2 32336 erdszelem5 32339 erdszelem8 32342 msrrcl 32687 mthmsta 32722 bdaydm 33141 icoreunrn 34522 icoreelrn 34524 relowlpssretop 34527 poimirlem26 34799 poimirlem27 34800 opnmbllem0 34809 dvtan 34823 seff 40518 sblpnf 40519 dvsconst 40539 dvsid 40540 dvsef 40541 expgrowth 40544 binomcxplemdvbinom 40562 binomcxplemdvsum 40564 binomcxplemnotnn0 40565 addcomgi 40665 dmuz 41380 dmico 41717 dvsinax 42073 fvvolioof 42151 fvvolicof 42153 dirkercncflem2 42266 fourierdlem42 42311 hoicvr 42707 ovolval3 42806 |
Copyright terms: Public domain | W3C validator |