Theorem fdmi 6747

Description: Inference associated with fdm 6745. 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

Step	Hyp	Ref	Expression
1		fdmi.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		fdm 6745	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1536  dom cdm 5688  ⟶wf 6558

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 207  df-an 396  df-fn 6565  df-f 6566

This theorem is referenced by:  f0cli  7117  rankvaln  9836  isnum2  9982  r0weon  10049  cfub  10286  cardcf  10289  cflecard  10290  cfle  10291  cflim2  10300  cfidm  10312  cardf  10587  smobeth  10623  inar1  10812  addcompq  10987  addcomnq  10988  mulcompq  10989  mulcomnq  10990  adderpq  10993  mulerpq  10994  addassnq  10995  mulassnq  10996  distrnq  10998  recmulnq  11001  recclnq  11003  dmrecnq  11005  lterpq  11007  ltanq  11008  ltmnq  11009  ltexnq  11012  nsmallnq  11014  ltbtwnnq  11015  prlem934  11070  ltaddpr  11071  ltexprlem2  11074  ltexprlem3  11075  ltexprlem4  11076  ltexprlem6  11078  ltexprlem7  11079  prlem936  11084  eluzel2  12880  uzssz  12896  elixx3g  13396  ndmioo  13410  elfz2  13550  fz0  13575  elfzoel1  13693  elfzoel2  13694  fzoval  13696  ltweuz  13998  fzofi  14011  dmhashres  14376  s1dm  14642  s2dm  14925  sumz  15754  sumss  15756  prod1  15976  prodss  15979  znnen  16244  unbenlem  16941  prmreclem6  16954  eldmcoa  18118  efgsdm  19762  efgsval  19763  efgsp1  19769  efgsfo  19771  efgredleme  19775  efgred  19780  gexex  19885  torsubg  19886  dmdprd  20032  dprdval  20037  iocpnfordt  23238  icomnfordt  23239  uzrest  23920  qtopbaslem  24794  retopbas  24796  tgqioo  24835  re2ndc  24836  bndth  25003  tcphcph  25284  ovolficcss  25517  ismbl  25574  uniiccdif  25626  dyadmbllem  25647  opnmbllem  25649  opnmblALT  25651  mbfimaopnlem  25703  itg1addlem4  25747  itg1addlem4OLD  25748  dvcmul  25995  dvcmulf  25996  dvexp  26005  c1liplem1  26049  deg1n0ima  26142  pserulm  26479  psercn2  26480  psercn2OLD  26481  psercnlem2  26482  psercnlem1  26483  psercn  26484  pserdvlem1  26485  pserdvlem2  26486  pserdv  26487  pserdv2  26488  abelth  26499  efcn  26501  efcvx  26507  eff1olem  26604  dvrelog  26693  logf1o2  26706  dvlog  26707  efopn  26714  logtayl  26716  cxpcn3lem  26804  cxpcn3  26805  resqrtcn  26806  atancl  26938  atanval  26941  dvatan  26992  atancn  26993  bdaydm  27833  lltropt  27925  madess  27929  oldssmade  27930  madebdayim  27940  oldbdayim  27941  lrold  27949  madefi  27964  oldfi  27965  topnfbey  30497  cnaddabloOLD  30609  cnidOLD  30610  cncvcOLD  30611  cnnv  30705  cnnvba  30707  cncph  30847  dfhnorm2  31150  hilablo  31188  hilid  31189  hilvc  31190  hhnv  31193  hhba  31195  hhph  31206  issh2  31237  hhssabloi  31290  hhssnv  31292  hhshsslem1  31295  imaelshi  32086  rnelshi  32087  nlelshi  32088  xrofsup  32777  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  coinfliprv  34463  erdszelem2  35176  erdszelem5  35179  erdszelem8  35182  msrrcl  35527  mthmsta  35562  icoreunrn  37341  icoreelrn  37343  relowlpssretop  37346  poimirlem26  37632  poimirlem27  37633  opnmbllem0  37642  dvtan  37656  fpwfvss  43401  seff  44304  sblpnf  44305  dvsconst  44325  dvsid  44326  dvsef  44327  expgrowth  44330  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  addcomgi  44451  dmuz  45176  dmico  45517  dvsinax  45868  fvvolioof  45944  fvvolicof  45946  dirkercncflem2  46059  fourierdlem42  46104  hoicvr  46503  ovolval3  46602