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

Theorem fdmi 6517
Description: Inference associated with fdm 6515. 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 6515 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2ax-mp 5 1 dom 𝐹 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  dom cdm 5548  wf 6344
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 208  df-an 397  df-fn 6351  df-f 6352
This theorem is referenced by:  f0cli  6856  rankvaln  9216  isnum2  9362  r0weon  9426  cfub  9659  cardcf  9662  cflecard  9663  cfle  9664  cflim2  9673  cfidm  9685  cardf  9960  smobeth  9996  inar1  10185  addcompq  10360  addcomnq  10361  mulcompq  10362  mulcomnq  10363  adderpq  10366  mulerpq  10367  addassnq  10368  mulassnq  10369  distrnq  10371  recmulnq  10374  recclnq  10376  dmrecnq  10378  lterpq  10380  ltanq  10381  ltmnq  10382  ltexnq  10385  nsmallnq  10387  ltbtwnnq  10388  prlem934  10443  ltaddpr  10444  ltexprlem2  10447  ltexprlem3  10448  ltexprlem4  10449  ltexprlem6  10451  ltexprlem7  10452  prlem936  10457  eluzel2  12236  uzssz  12252  elixx3g  12739  ndmioo  12753  elfz2  12887  fz0  12910  elfzoel1  13024  elfzoel2  13025  fzoval  13027  ltweuz  13317  fzofi  13330  dmhashres  13689  s1dm  13950  s2dm  14240  sumz  15067  sumss  15069  prod1  15286  prodss  15289  znnen  15553  unbenlem  16232  prmreclem6  16245  eldmcoa  17313  efgsdm  18785  efgsval  18786  efgsp1  18792  efgsfo  18794  efgredleme  18798  efgred  18803  gexex  18902  torsubg  18903  dmdprd  19049  dprdval  19054  iocpnfordt  21751  icomnfordt  21752  uzrest  22433  qtopbaslem  23294  retopbas  23296  tgqioo  23335  re2ndc  23336  bndth  23489  tcphcph  23767  ovolficcss  23997  ismbl  24054  uniiccdif  24106  dyadmbllem  24127  opnmbllem  24129  opnmblALT  24131  mbfimaopnlem  24183  itg1addlem4  24227  dvcmul  24468  dvcmulf  24469  dvexp  24477  c1liplem1  24520  deg1n0ima  24610  pserulm  24937  psercn2  24938  psercnlem2  24939  psercnlem1  24940  psercn  24941  pserdvlem1  24942  pserdvlem2  24943  pserdv  24944  pserdv2  24945  abelth  24956  efcn  24958  efcvx  24964  eff1olem  25059  dvrelog  25147  logf1o2  25160  dvlog  25161  efopn  25168  logtayl  25170  cxpcn3lem  25255  cxpcn3  25256  resqrtcn  25257  atancl  25386  atanval  25389  dvatan  25440  atancn  25441  topnfbey  28175  cnaddabloOLD  28285  cnidOLD  28286  cncvcOLD  28287  cnnv  28381  cnnvba  28383  cncph  28523  dfhnorm2  28826  hilablo  28864  hilid  28865  hilvc  28866  hhnv  28869  hhba  28871  hhph  28882  issh2  28913  hhssabloi  28966  hhssnv  28968  hhshsslem1  28971  imaelshi  29762  rnelshi  29763  nlelshi  29764  xrofsup  30418  coinfliprv  31639  erdszelem2  32336  erdszelem5  32339  erdszelem8  32342  msrrcl  32687  mthmsta  32722  bdaydm  33141  icoreunrn  34522  icoreelrn  34524  relowlpssretop  34527  poimirlem26  34799  poimirlem27  34800  opnmbllem0  34809  dvtan  34823  seff  40518  sblpnf  40519  dvsconst  40539  dvsid  40540  dvsef  40541  expgrowth  40544  binomcxplemdvbinom  40562  binomcxplemdvsum  40564  binomcxplemnotnn0  40565  addcomgi  40665  dmuz  41380  dmico  41717  dvsinax  42073  fvvolioof  42151  fvvolicof  42153  dirkercncflem2  42266  fourierdlem42  42311  hoicvr  42707  ovolval3  42806
  Copyright terms: Public domain W3C validator