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

Theorem fdmi 5410
Description: The domain of a mapping. (Contributed by NM, 28-Jul-2008.)
Hypothesis
Ref Expression
fdmi.1  |-  F : A
--> B
Assertion
Ref Expression
fdmi  |-  dom  F  =  A

Proof of Theorem fdmi
StepHypRef Expression
1 fdmi.1 . 2  |-  F : A
--> B
2 fdm 5409 . 2  |-  ( F : A --> B  ->  dom  F  =  A )
31, 2ax-mp 8 1  |-  dom  F  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632   dom cdm 4705   -->wf 5267
This theorem is referenced by:  f0cli  5687  rankvaln  7487  isnum2  7594  r0weon  7656  cfub  7891  cardcf  7894  cflecard  7895  cfle  7896  cflim2  7905  cfidm  7917  cardf  8188  smobeth  8224  inar1  8413  addcompq  8590  addcomnq  8591  mulcompq  8592  mulcomnq  8593  adderpq  8596  mulerpq  8597  addassnq  8598  mulassnq  8599  distrnq  8601  recmulnq  8604  recclnq  8606  dmrecnq  8608  lterpq  8610  ltanq  8611  ltmnq  8612  ltexnq  8615  nsmallnq  8617  ltbtwnnq  8618  prlem934  8673  ltaddpr  8674  ltexprlem2  8677  ltexprlem3  8678  ltexprlem4  8679  ltexprlem6  8681  ltexprlem7  8682  prlem936  8687  eluzel2  10251  uzssz  10263  elixx3g  10685  ndmioo  10699  elfz2  10805  elfzoel1  10889  elfzoel2  10890  fzoval  10892  ltweuz  11040  fzofi  11052  sumz  12211  sumss  12213  znnen  12507  unbenlem  12971  prmreclem6  12984  eldmcoa  13913  efgsdm  15055  efgsval  15056  efgsp1  15062  efgsfo  15064  efgredleme  15068  efgred  15073  gexex  15161  torsubg  15162  dmdprd  15252  dprdval  15254  iocpnfordt  16961  icomnfordt  16962  uzrest  17608  qtopbaslem  18283  retopbas  18285  tgqioo  18322  re2ndc  18323  bndth  18472  tchcph  18683  ovolficcss  18845  ismbl  18901  uniiccdif  18949  dyadmbllem  18970  opnmbllem  18972  opnmblALT  18974  mbfimaopnlem  19026  itg1addlem4  19070  dvcmul  19309  dvcmulf  19310  dvexp  19318  c1liplem1  19359  deg1n0ima  19491  pserulm  19814  psercn2  19815  psercnlem2  19816  psercnlem1  19817  psercn  19818  pserdvlem1  19819  pserdvlem2  19820  pserdv  19821  pserdv2  19822  abelth  19833  efcn  19835  efcvx  19841  eff1olem  19926  dvrelog  20000  logf1o2  20013  dvlog  20014  efopn  20021  logtayl  20023  cxpcn3lem  20103  cxpcn3  20104  resqrcn  20105  atancl  20193  atanval  20196  dvatan  20247  atancn  20248  cnaddablo  21033  cnid  21034  addinv  21035  readdsubgo  21036  zaddsubgo  21037  ablomul  21038  mulid  21039  efghgrp  21056  cnrngo  21086  cncvc  21155  cnnv  21261  cnnvba  21263  cncph  21413  dfhnorm2  21717  hilablo  21755  hilid  21756  hilvc  21757  hhnv  21760  hhba  21762  hhph  21773  issh2  21804  hhssabloi  21855  hhssnv  21857  hhshsslem1  21860  imaelshi  22654  rnelshi  22655  nlelshi  22656  measbase  23543  erdszelem2  23738  erdszelem5  23741  erdszelem8  23744  prod1  24169  bdaydm  24403  nZdef  25283  seff  27641  sblpnf  27642  dvsconst  27650  dvsid  27651  dvsef  27652  expgrowth  27655  addcomgi  27764
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5274  df-f 5275
  Copyright terms: Public domain W3C validator