![]() |
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 6301. 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 6301 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐹 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 dom cdm 5357 ⟶wf 6133 |
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 199 df-an 387 df-fn 6140 df-f 6141 |
This theorem is referenced by: f0cli 6636 rankvaln 8961 isnum2 9106 r0weon 9170 cfub 9408 cardcf 9411 cflecard 9412 cfle 9413 cflim2 9422 cfidm 9434 cardf 9709 smobeth 9745 inar1 9934 addcompq 10109 addcomnq 10110 mulcompq 10111 mulcomnq 10112 adderpq 10115 mulerpq 10116 addassnq 10117 mulassnq 10118 distrnq 10120 recmulnq 10123 recclnq 10125 dmrecnq 10127 lterpq 10129 ltanq 10130 ltmnq 10131 ltexnq 10134 nsmallnq 10136 ltbtwnnq 10137 prlem934 10192 ltaddpr 10193 ltexprlem2 10196 ltexprlem3 10197 ltexprlem4 10198 ltexprlem6 10200 ltexprlem7 10201 prlem936 10206 eluzel2 12001 uzssz 12016 elixx3g 12504 ndmioo 12518 elfz2 12654 fz0 12677 elfzoel1 12791 elfzoel2 12792 fzoval 12794 ltweuz 13083 fzofi 13096 dmhashres 13450 s1dm 13702 s2dm 14045 sumz 14864 sumss 14866 prod1 15081 prodss 15084 znnen 15349 unbenlem 16020 prmreclem6 16033 eldmcoa 17104 efgsdm 18531 efgsval 18532 efgsp1 18538 efgsfo 18541 efgredleme 18545 efgred 18551 gexex 18646 torsubg 18647 dmdprd 18788 dprdval 18793 iocpnfordt 21431 icomnfordt 21432 uzrest 22113 qtopbaslem 22974 retopbas 22976 tgqioo 23015 re2ndc 23016 bndth 23169 tcphcph 23447 ovolficcss 23677 ismbl 23734 uniiccdif 23786 dyadmbllem 23807 opnmbllem 23809 opnmblALT 23811 mbfimaopnlem 23863 itg1addlem4 23907 dvcmul 24148 dvcmulf 24149 dvexp 24157 c1liplem1 24200 deg1n0ima 24290 pserulm 24617 psercn2 24618 psercnlem2 24619 psercnlem1 24620 psercn 24621 pserdvlem1 24622 pserdvlem2 24623 pserdv 24624 pserdv2 24625 abelth 24636 efcn 24638 efcvx 24644 eff1olem 24736 dvrelog 24824 logf1o2 24837 dvlog 24838 efopn 24845 logtayl 24847 cxpcn3lem 24932 cxpcn3 24933 resqrtcn 24934 atancl 25063 atanval 25066 dvatan 25117 atancn 25118 topnfbey 27904 cnaddabloOLD 28012 cnidOLD 28013 cncvcOLD 28014 cnnv 28108 cnnvba 28110 cncph 28250 dfhnorm2 28555 hilablo 28593 hilid 28594 hilvc 28595 hhnv 28598 hhba 28600 hhph 28611 issh2 28642 hhssabloi 28695 hhssnv 28697 hhshsslem1 28700 imaelshi 29493 rnelshi 29494 nlelshi 29495 xrofsup 30102 coinfliprv 31147 erdszelem2 31777 erdszelem5 31780 erdszelem8 31783 msrrcl 32043 mthmsta 32078 bdaydm 32483 icoreunrn 33805 icoreelrn 33807 relowlpssretop 33810 poimirlem26 34066 poimirlem27 34067 opnmbllem0 34076 dvtan 34090 seff 39474 sblpnf 39475 dvsconst 39495 dvsid 39496 dvsef 39497 expgrowth 39500 binomcxplemdvbinom 39518 binomcxplemdvsum 39520 binomcxplemnotnn0 39521 addcomgi 39624 dmuz 40367 dmico 40710 dvsinax 41065 fvvolioof 41143 fvvolicof 41145 dirkercncflem2 41258 fourierdlem42 41303 hoicvr 41699 ovolval3 41798 |
Copyright terms: Public domain | W3C validator |