| 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 6745. 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 6745 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐹 = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 dom cdm 5685 ⟶wf 6557 |
| 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 df-f 6565 |
| This theorem is referenced by: f0cli 7118 rankvaln 9839 isnum2 9985 r0weon 10052 cfub 10289 cardcf 10292 cflecard 10293 cfle 10294 cflim2 10303 cfidm 10315 cardf 10590 smobeth 10626 inar1 10815 addcompq 10990 addcomnq 10991 mulcompq 10992 mulcomnq 10993 adderpq 10996 mulerpq 10997 addassnq 10998 mulassnq 10999 distrnq 11001 recmulnq 11004 recclnq 11006 dmrecnq 11008 lterpq 11010 ltanq 11011 ltmnq 11012 ltexnq 11015 nsmallnq 11017 ltbtwnnq 11018 prlem934 11073 ltaddpr 11074 ltexprlem2 11077 ltexprlem3 11078 ltexprlem4 11079 ltexprlem6 11081 ltexprlem7 11082 prlem936 11087 eluzel2 12883 uzssz 12899 elixx3g 13400 ndmioo 13414 elfz2 13554 fz0 13579 elfzoel1 13697 elfzoel2 13698 fzoval 13700 ltweuz 14002 fzofi 14015 dmhashres 14380 s1dm 14646 s2dm 14929 sumz 15758 sumss 15760 prod1 15980 prodss 15983 znnen 16248 unbenlem 16946 prmreclem6 16959 eldmcoa 18110 efgsdm 19748 efgsval 19749 efgsp1 19755 efgsfo 19757 efgredleme 19761 efgred 19766 gexex 19871 torsubg 19872 dmdprd 20018 dprdval 20023 iocpnfordt 23223 icomnfordt 23224 uzrest 23905 qtopbaslem 24779 retopbas 24781 tgqioo 24821 re2ndc 24822 bndth 24990 tcphcph 25271 ovolficcss 25504 ismbl 25561 uniiccdif 25613 dyadmbllem 25634 opnmbllem 25636 opnmblALT 25638 mbfimaopnlem 25690 itg1addlem4 25734 dvcmul 25981 dvcmulf 25982 dvexp 25991 c1liplem1 26035 deg1n0ima 26128 pserulm 26465 psercn2 26466 psercn2OLD 26467 psercnlem2 26468 psercnlem1 26469 psercn 26470 pserdvlem1 26471 pserdvlem2 26472 pserdv 26473 pserdv2 26474 abelth 26485 efcn 26487 efcvx 26493 eff1olem 26590 dvrelog 26679 logf1o2 26692 dvlog 26693 efopn 26700 logtayl 26702 cxpcn3lem 26790 cxpcn3 26791 resqrtcn 26792 atancl 26924 atanval 26927 dvatan 26978 atancn 26979 bdaydm 27819 lltropt 27911 madess 27915 oldssmade 27916 madebdayim 27926 oldbdayim 27927 lrold 27935 madefi 27950 oldfi 27951 topnfbey 30488 cnaddabloOLD 30600 cnidOLD 30601 cncvcOLD 30602 cnnv 30696 cnnvba 30698 cncph 30838 dfhnorm2 31141 hilablo 31179 hilid 31180 hilvc 31181 hhnv 31184 hhba 31186 hhph 31197 issh2 31228 hhssabloi 31281 hhssnv 31283 hhshsslem1 31286 imaelshi 32077 rnelshi 32078 nlelshi 32079 xrofsup 32771 ply1degltel 33615 ply1degleel 33616 ply1degltlss 33617 coinfliprv 34485 erdszelem2 35197 erdszelem5 35200 erdszelem8 35203 msrrcl 35548 mthmsta 35583 icoreunrn 37360 icoreelrn 37362 relowlpssretop 37365 poimirlem26 37653 poimirlem27 37654 opnmbllem0 37663 dvtan 37677 fpwfvss 43425 seff 44328 sblpnf 44329 dvsconst 44349 dvsid 44350 dvsef 44351 expgrowth 44354 binomcxplemdvbinom 44372 binomcxplemdvsum 44374 binomcxplemnotnn0 44375 addcomgi 44475 dmuz 45239 dmico 45578 dvsinax 45928 fvvolioof 46004 fvvolicof 46006 dirkercncflem2 46119 fourierdlem42 46164 hoicvr 46563 ovolval3 46662 fucofvalne 49020 |
| Copyright terms: Public domain | W3C validator |