MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fdmi Unicode version

Theorem fdmi 5741
Description: The domain of a mapping. (Contributed by NM, 28-Jul-2008.)
Hypothesis
Ref Expression
fdmi.1
Assertion
Ref Expression
fdmi

Proof of Theorem fdmi
StepHypRef Expression
1 fdmi.1 . 2
2 fdm 5740 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  domcdm 5004  -->wf 5589
This theorem is referenced by:  f0cli  6042  rankvaln  8238  isnum2  8347  r0weon  8411  cfub  8650  cardcf  8653  cflecard  8654  cfle  8655  cflim2  8664  cfidm  8676  cardf  8946  smobeth  8982  inar1  9174  addcompq  9349  addcomnq  9350  mulcompq  9351  mulcomnq  9352  adderpq  9355  mulerpq  9356  addassnq  9357  mulassnq  9358  distrnq  9360  recmulnq  9363  recclnq  9365  dmrecnq  9367  lterpq  9369  ltanq  9370  ltmnq  9371  ltexnq  9374  nsmallnq  9376  ltbtwnnq  9377  prlem934  9432  ltaddpr  9433  ltexprlem2  9436  ltexprlem3  9437  ltexprlem4  9438  ltexprlem6  9440  ltexprlem7  9441  prlem936  9446  eluzel2  11115  uzssz  11129  elixx3g  11571  ndmioo  11585  elfz2  11708  fz0  11730  elfzoel1  11827  elfzoel2  11828  fzoval  11830  ltweuz  12072  fzofi  12084  dmhashres  12414  sumz  13544  sumss  13546  prod1  13751  prodss  13754  znnen  13946  unbenlem  14426  prmreclem6  14439  eldmcoa  15392  efgsdm  16748  efgsval  16749  efgsp1  16755  efgsfo  16757  efgredleme  16761  efgred  16766  gexex  16859  torsubg  16860  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  iocpnfordt  19716  icomnfordt  19717  uzrest  20398  qtopbaslem  21265  retopbas  21267  tgqioo  21305  re2ndc  21306  bndth  21458  tchcph  21680  ovolficcss  21881  ismbl  21937  uniiccdif  21987  dyadmbllem  22008  opnmbllem  22010  opnmblALT  22012  mbfimaopnlem  22062  itg1addlem4  22106  dvcmul  22347  dvcmulf  22348  dvexp  22356  c1liplem1  22397  deg1n0ima  22489  pserulm  22817  psercn2  22818  psercnlem2  22819  psercnlem1  22820  psercn  22821  pserdvlem1  22822  pserdvlem2  22823  pserdv  22824  pserdv2  22825  abelth  22836  efcn  22838  efcvx  22844  eff1olem  22935  dvrelog  23018  logf1o2  23031  dvlog  23032  efopn  23039  logtayl  23041  cxpcn3lem  23121  cxpcn3  23122  resqrtcn  23123  atancl  23212  atanval  23215  dvatan  23266  atancn  23267  cnaddablo  25352  cnid  25353  addinv  25354  readdsubgo  25355  zaddsubgo  25356  ablomul  25357  mulid  25358  efghgrpOLD  25375  cnrngo  25405  cncvc  25476  cnnv  25582  cnnvba  25584  cncph  25734  dfhnorm2  26039  hilablo  26077  hilid  26078  hilvc  26079  hhnv  26082  hhba  26084  hhph  26095  issh2  26126  hhssabloi  26178  hhssnv  26180  hhshsslem1  26183  imaelshi  26977  rnelshi  26978  nlelshi  26979  xrofsup  27582  coinfliprv  28421  erdszelem2  28636  erdszelem5  28639  erdszelem8  28642  msrrcl  28903  mthmsta  28938  bdaydm  29438  opnmbllem0  30050  dvtan  30065  seff  31189  sblpnf  31190  dvsconst  31235  dvsid  31236  dvsef  31237  expgrowth  31240  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  addcomgi  31365  dvsinax  31708  dirkercncflem2  31886  fourierdlem42  31931
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 185  df-an 371  df-fn 5596  df-f 5597
  Copyright terms: Public domain W3C validator