Theorem fdmi 6667

Description: Inference associated with fdm 6665. 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 6665	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1540  dom cdm 5623  ⟶wf 6482

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 6489  df-f 6490

This theorem is referenced by:  f0cli  7036  rankvaln  9714  isnum2  9860  r0weon  9925  cfub  10162  cardcf  10165  cflecard  10166  cfle  10167  cflim2  10176  cfidm  10188  cardf  10463  smobeth  10499  inar1  10688  addcompq  10863  addcomnq  10864  mulcompq  10865  mulcomnq  10866  adderpq  10869  mulerpq  10870  addassnq  10871  mulassnq  10872  distrnq  10874  recmulnq  10877  recclnq  10879  dmrecnq  10881  lterpq  10883  ltanq  10884  ltmnq  10885  ltexnq  10888  nsmallnq  10890  ltbtwnnq  10891  prlem934  10946  ltaddpr  10947  ltexprlem2  10950  ltexprlem3  10951  ltexprlem4  10952  ltexprlem6  10954  ltexprlem7  10955  prlem936  10960  eluzel2  12758  uzssz  12774  elixx3g  13279  ndmioo  13293  elfz2  13435  fz0  13460  elfzoel1  13578  elfzoel2  13579  fzoval  13581  ltweuz  13886  fzofi  13899  dmhashres  14266  s1dm  14533  s2dm  14815  sumz  15647  sumss  15649  prod1  15869  prodss  15872  znnen  16139  unbenlem  16838  prmreclem6  16851  eldmcoa  17990  efgsdm  19627  efgsval  19628  efgsp1  19634  efgsfo  19636  efgredleme  19640  efgred  19645  gexex  19750  torsubg  19751  dmdprd  19897  dprdval  19902  iocpnfordt  23118  icomnfordt  23119  uzrest  23800  qtopbaslem  24662  retopbas  24664  tgqioo  24704  re2ndc  24705  bndth  24873  tcphcph  25153  ovolficcss  25386  ismbl  25443  uniiccdif  25495  dyadmbllem  25516  opnmbllem  25518  opnmblALT  25520  mbfimaopnlem  25572  itg1addlem4  25616  dvcmul  25863  dvcmulf  25864  dvexp  25873  c1liplem1  25917  deg1n0ima  26010  pserulm  26347  psercn2  26348  psercn2OLD  26349  psercnlem2  26350  psercnlem1  26351  psercn  26352  pserdvlem1  26353  pserdvlem2  26354  pserdv  26355  pserdv2  26356  abelth  26367  efcn  26369  efcvx  26375  eff1olem  26473  dvrelog  26562  logf1o2  26575  dvlog  26576  efopn  26583  logtayl  26585  cxpcn3lem  26673  cxpcn3  26674  resqrtcn  26675  atancl  26807  atanval  26810  dvatan  26861  atancn  26862  bdaydm  27702  lltropt  27804  madess  27808  oldssmade  27809  oldss  27810  madebdayim  27820  oldbdayim  27821  lrold  27829  madefi  27845  oldfi  27846  topnfbey  30431  cnaddabloOLD  30543  cnidOLD  30544  cncvcOLD  30545  cnnv  30639  cnnvba  30641  cncph  30781  dfhnorm2  31084  hilablo  31122  hilid  31123  hilvc  31124  hhnv  31127  hhba  31129  hhph  31140  issh2  31171  hhssabloi  31224  hhssnv  31226  hhshsslem1  31229  imaelshi  32020  rnelshi  32021  nlelshi  32022  xrofsup  32723  ply1degltel  33536  ply1degleel  33537  ply1degltlss  33538  coinfliprv  34450  erdszelem2  35164  erdszelem5  35167  erdszelem8  35170  msrrcl  35515  mthmsta  35550  icoreunrn  37332  icoreelrn  37334  relowlpssretop  37337  poimirlem26  37625  poimirlem27  37626  opnmbllem0  37635  dvtan  37649  fpwfvss  43385  seff  44282  sblpnf  44283  dvsconst  44303  dvsid  44304  dvsef  44305  expgrowth  44308  binomcxplemdvbinom  44326  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  addcomgi  44429  dmuz  45212  dmico  45545  dvsinax  45895  fvvolioof  45971  fvvolicof  45973  dirkercncflem2  46086  fourierdlem42  46131  hoicvr  46530  ovolval3  46629  sinnpoly  46876  fucofvalne  49298