![]() |
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 6732. 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 6732 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐹 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 dom cdm 5678 ⟶wf 6545 |
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 206 df-an 395 df-fn 6552 df-f 6553 |
This theorem is referenced by: f0cli 7107 rankvaln 9824 isnum2 9970 r0weon 10037 cfub 10274 cardcf 10277 cflecard 10278 cfle 10279 cflim2 10288 cfidm 10300 cardf 10575 smobeth 10611 inar1 10800 addcompq 10975 addcomnq 10976 mulcompq 10977 mulcomnq 10978 adderpq 10981 mulerpq 10982 addassnq 10983 mulassnq 10984 distrnq 10986 recmulnq 10989 recclnq 10991 dmrecnq 10993 lterpq 10995 ltanq 10996 ltmnq 10997 ltexnq 11000 nsmallnq 11002 ltbtwnnq 11003 prlem934 11058 ltaddpr 11059 ltexprlem2 11062 ltexprlem3 11063 ltexprlem4 11064 ltexprlem6 11066 ltexprlem7 11067 prlem936 11072 eluzel2 12860 uzssz 12876 elixx3g 13372 ndmioo 13386 elfz2 13526 fz0 13551 elfzoel1 13665 elfzoel2 13666 fzoval 13668 ltweuz 13962 fzofi 13975 dmhashres 14336 s1dm 14594 s2dm 14877 sumz 15704 sumss 15706 prod1 15924 prodss 15927 znnen 16192 unbenlem 16880 prmreclem6 16893 eldmcoa 18057 efgsdm 19697 efgsval 19698 efgsp1 19704 efgsfo 19706 efgredleme 19710 efgred 19715 gexex 19820 torsubg 19821 dmdprd 19967 dprdval 19972 iocpnfordt 23163 icomnfordt 23164 uzrest 23845 qtopbaslem 24719 retopbas 24721 tgqioo 24760 re2ndc 24761 bndth 24928 tcphcph 25209 ovolficcss 25442 ismbl 25499 uniiccdif 25551 dyadmbllem 25572 opnmbllem 25574 opnmblALT 25576 mbfimaopnlem 25628 itg1addlem4 25672 itg1addlem4OLD 25673 dvcmul 25919 dvcmulf 25920 dvexp 25929 c1liplem1 25973 deg1n0ima 26069 pserulm 26403 psercn2 26404 psercn2OLD 26405 psercnlem2 26406 psercnlem1 26407 psercn 26408 pserdvlem1 26409 pserdvlem2 26410 pserdv 26411 pserdv2 26412 abelth 26423 efcn 26425 efcvx 26431 eff1olem 26527 dvrelog 26616 logf1o2 26629 dvlog 26630 efopn 26637 logtayl 26639 cxpcn3lem 26727 cxpcn3 26728 resqrtcn 26729 atancl 26858 atanval 26861 dvatan 26912 atancn 26913 bdaydm 27753 lltropt 27845 madess 27849 oldssmade 27850 madebdayim 27860 oldbdayim 27861 lrold 27869 topnfbey 30351 cnaddabloOLD 30463 cnidOLD 30464 cncvcOLD 30465 cnnv 30559 cnnvba 30561 cncph 30701 dfhnorm2 31004 hilablo 31042 hilid 31043 hilvc 31044 hhnv 31047 hhba 31049 hhph 31060 issh2 31091 hhssabloi 31144 hhssnv 31146 hhshsslem1 31149 imaelshi 31940 rnelshi 31941 nlelshi 31942 xrofsup 32619 ply1degltel 33396 ply1degleel 33397 ply1degltlss 33398 coinfliprv 34233 erdszelem2 34933 erdszelem5 34936 erdszelem8 34939 msrrcl 35284 mthmsta 35319 icoreunrn 36969 icoreelrn 36971 relowlpssretop 36974 poimirlem26 37250 poimirlem27 37251 opnmbllem0 37260 dvtan 37274 fpwfvss 42984 seff 43888 sblpnf 43889 dvsconst 43909 dvsid 43910 dvsef 43911 expgrowth 43914 binomcxplemdvbinom 43932 binomcxplemdvsum 43934 binomcxplemnotnn0 43935 addcomgi 44035 dmuz 44746 dmico 45088 dvsinax 45439 fvvolioof 45515 fvvolicof 45517 dirkercncflem2 45630 fourierdlem42 45675 hoicvr 46074 ovolval3 46173 |
Copyright terms: Public domain | W3C validator |