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

Theorem fdmi 6090
Description: The domain of a mapping. (Contributed by NM, 28-Jul-2008.)
Hypothesis
Ref Expression
fdmi.1 𝐹:𝐴𝐵
Assertion
Ref Expression
fdmi dom 𝐹 = 𝐴

Proof of Theorem fdmi
StepHypRef Expression
1 fdmi.1 . 2 𝐹:𝐴𝐵
2 fdm 6089 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2ax-mp 5 1 dom 𝐹 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  dom cdm 5143  wf 5922
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 197  df-an 385  df-fn 5929  df-f 5930
This theorem is referenced by:  f0cli  6410  rankvaln  8700  isnum2  8809  r0weon  8873  cfub  9109  cardcf  9112  cflecard  9113  cfle  9114  cflim2  9123  cfidm  9135  cardf  9410  smobeth  9446  inar1  9635  addcompq  9810  addcomnq  9811  mulcompq  9812  mulcomnq  9813  adderpq  9816  mulerpq  9817  addassnq  9818  mulassnq  9819  distrnq  9821  recmulnq  9824  recclnq  9826  dmrecnq  9828  lterpq  9830  ltanq  9831  ltmnq  9832  ltexnq  9835  nsmallnq  9837  ltbtwnnq  9838  prlem934  9893  ltaddpr  9894  ltexprlem2  9897  ltexprlem3  9898  ltexprlem4  9899  ltexprlem6  9901  ltexprlem7  9902  prlem936  9907  eluzel2  11730  uzssz  11745  elixx3g  12226  ndmioo  12240  elfz2  12371  fz0  12394  elfzoel1  12507  elfzoel2  12508  fzoval  12510  ltweuz  12800  fzofi  12813  dmhashres  13169  s1dm  13425  s2dm  13681  sumz  14497  sumss  14499  prod1  14718  prodss  14721  znnen  14985  unbenlem  15659  prmreclem6  15672  eldmcoa  16762  efgsdm  18189  efgsval  18190  efgsp1  18196  efgsfo  18198  efgredleme  18202  efgred  18207  gexex  18302  torsubg  18303  dmdprd  18443  dprdval  18448  iocpnfordt  21067  icomnfordt  21068  uzrest  21748  qtopbaslem  22609  retopbas  22611  tgqioo  22650  re2ndc  22651  bndth  22804  tchcph  23082  ovolficcss  23284  ismbl  23340  uniiccdif  23392  dyadmbllem  23413  opnmbllem  23415  opnmblALT  23417  mbfimaopnlem  23467  itg1addlem4  23511  dvcmul  23752  dvcmulf  23753  dvexp  23761  c1liplem1  23804  deg1n0ima  23894  pserulm  24221  psercn2  24222  psercnlem2  24223  psercnlem1  24224  psercn  24225  pserdvlem1  24226  pserdvlem2  24227  pserdv  24228  pserdv2  24229  abelth  24240  efcn  24242  efcvx  24248  eff1olem  24339  dvrelog  24428  logf1o2  24441  dvlog  24442  efopn  24449  logtayl  24451  cxpcn3lem  24533  cxpcn3  24534  resqrtcn  24535  atancl  24653  atanval  24656  dvatan  24707  atancn  24708  topnfbey  27455  cnaddabloOLD  27564  cnidOLD  27565  cncvcOLD  27566  cnnv  27660  cnnvba  27662  cncph  27802  dfhnorm2  28107  hilablo  28145  hilid  28146  hilvc  28147  hhnv  28150  hhba  28152  hhph  28163  issh2  28194  hhssabloi  28247  hhssnv  28249  hhshsslem1  28252  imaelshi  29045  rnelshi  29046  nlelshi  29047  xrofsup  29661  coinfliprv  30672  erdszelem2  31300  erdszelem5  31303  erdszelem8  31306  msrrcl  31566  mthmsta  31601  bdaydm  32015  icoreunrn  33337  icoreelrn  33339  relowlpssretop  33342  poimirlem26  33565  poimirlem27  33566  opnmbllem0  33575  dvtan  33590  seff  38825  sblpnf  38826  dvsconst  38846  dvsid  38847  dvsef  38848  expgrowth  38851  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  addcomgi  38977  dmuz  39754  dmico  40110  dvsinax  40445  fvvolioof  40524  fvvolicof  40526  dirkercncflem2  40639  fourierdlem42  40684  hoicvr  41083  ovolval3  41182
  Copyright terms: Public domain W3C validator