![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fdmi | Structured version Visualization version Unicode version |
Description: The domain of a mapping. (Contributed by NM, 28-Jul-2008.) |
Ref | Expression |
---|---|
fdmi.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fdmi |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdmi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fdm 5731 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 189 df-an 373 df-fn 5584 df-f 5585 |
This theorem is referenced by: f0cli 6031 rankvaln 8267 isnum2 8376 r0weon 8440 cfub 8676 cardcf 8679 cflecard 8680 cfle 8681 cflim2 8690 cfidm 8702 cardf 8972 smobeth 9008 inar1 9197 addcompq 9372 addcomnq 9373 mulcompq 9374 mulcomnq 9375 adderpq 9378 mulerpq 9379 addassnq 9380 mulassnq 9381 distrnq 9383 recmulnq 9386 recclnq 9388 dmrecnq 9390 lterpq 9392 ltanq 9393 ltmnq 9394 ltexnq 9397 nsmallnq 9399 ltbtwnnq 9400 prlem934 9455 ltaddpr 9456 ltexprlem2 9459 ltexprlem3 9460 ltexprlem4 9461 ltexprlem6 9463 ltexprlem7 9464 prlem936 9469 eluzel2 11161 uzssz 11175 elixx3g 11645 ndmioo 11660 elfz2 11788 fz0 11811 elfzoel1 11915 elfzoel2 11916 fzoval 11918 ltweuz 12172 fzofi 12184 dmhashres 12521 sumz 13781 sumss 13783 prod1 13991 prodss 13994 znnen 14258 unbenlem 14845 prmreclem6 14858 eldmcoa 15953 efgsdm 17373 efgsval 17374 efgsp1 17380 efgsfo 17382 efgredleme 17386 efgred 17391 gexex 17484 torsubg 17485 dmdprd 17623 dprdval 17628 iocpnfordt 20224 icomnfordt 20225 uzrest 20905 qtopbaslem 21772 retopbas 21774 tgqioo 21811 re2ndc 21812 bndth 21979 tchcph 22204 ovolficcss 22415 ismbl 22473 uniiccdif 22528 dyadmbllem 22550 opnmbllem 22552 opnmblALT 22554 mbfimaopnlem 22604 itg1addlem4 22650 dvcmul 22891 dvcmulf 22892 dvexp 22900 c1liplem1 22941 deg1n0ima 23031 pserulm 23370 psercn2 23371 psercnlem2 23372 psercnlem1 23373 psercn 23374 pserdvlem1 23375 pserdvlem2 23376 pserdv 23377 pserdv2 23378 abelth 23389 efcn 23391 efcvx 23397 eff1olem 23490 dvrelog 23575 logf1o2 23588 dvlog 23589 efopn 23596 logtayl 23598 cxpcn3lem 23680 cxpcn3 23681 resqrtcn 23682 atancl 23800 atanval 23803 dvatan 23854 atancn 23855 topnfbey 25899 cnaddablo 26071 cnid 26072 addinv 26073 readdsubgo 26074 zaddsubgo 26075 ablomul 26076 mulid 26077 efghgrpOLD 26094 cnrngo 26124 cncvc 26195 cnnv 26301 cnnvba 26303 cncph 26453 dfhnorm2 26768 hilablo 26806 hilid 26807 hilvc 26808 hhnv 26811 hhba 26813 hhph 26824 issh2 26855 hhssabloi 26906 hhssnv 26908 hhshsslem1 26911 imaelshi 27704 rnelshi 27705 nlelshi 27706 xrofsup 28346 coinfliprv 29308 erdszelem2 29908 erdszelem5 29911 erdszelem8 29914 msrrcl 30174 mthmsta 30209 bdaydm 30560 icoreunrn 31755 icoreelrn 31757 relowlpssretop 31760 poimirlem26 31959 poimirlem27 31960 opnmbllem0 31969 dvtan 31985 seff 36651 sblpnf 36652 dvsconst 36673 dvsid 36674 dvsef 36675 expgrowth 36678 binomcxplemdvbinom 36696 binomcxplemdvsum 36698 binomcxplemnotnn0 36699 addcomgi 36803 dvsinax 37777 dirkercncflem2 37960 fourierdlem42 38006 fourierdlem42OLD 38007 hoicvr 38364 |
Copyright terms: Public domain | W3C validator |