Theorem fdmi 6671

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

Syntax hints:   = wceq 1542  dom cdm 5622  ⟶wf 6486

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 6493  df-f 6494

This theorem is referenced by:  f0cli  7042  rankvaln  9712  isnum2  9858  r0weon  9923  cfub  10160  cardcf  10163  cflecard  10164  cfle  10165  cflim2  10174  cfidm  10186  cardf  10461  smobeth  10498  inar1  10687  addcompq  10862  addcomnq  10863  mulcompq  10864  mulcomnq  10865  adderpq  10868  mulerpq  10869  addassnq  10870  mulassnq  10871  distrnq  10873  recmulnq  10876  recclnq  10878  dmrecnq  10880  lterpq  10882  ltanq  10883  ltmnq  10884  ltexnq  10887  nsmallnq  10889  ltbtwnnq  10890  prlem934  10945  ltaddpr  10946  ltexprlem2  10949  ltexprlem3  10950  ltexprlem4  10951  ltexprlem6  10953  ltexprlem7  10954  prlem936  10959  eluzel2  12782  uzssz  12798  elixx3g  13300  ndmioo  13314  elfz2  13457  fz0  13482  elfzoel1  13600  elfzoel2  13601  fzoval  13603  ltweuz  13912  fzofi  13925  dmhashres  14292  s1dm  14560  s2dm  14841  sumz  15673  sumss  15675  prod1  15898  prodss  15901  znnen  16168  unbenlem  16868  prmreclem6  16881  eldmcoa  18021  efgsdm  19694  efgsval  19695  efgsp1  19701  efgsfo  19703  efgredleme  19707  efgred  19712  gexex  19817  torsubg  19818  dmdprd  19964  dprdval  19969  iocpnfordt  23189  icomnfordt  23190  uzrest  23871  qtopbaslem  24732  retopbas  24734  tgqioo  24774  re2ndc  24775  bndth  24934  tcphcph  25213  ovolficcss  25445  ismbl  25502  uniiccdif  25554  dyadmbllem  25575  opnmbllem  25577  opnmblALT  25579  mbfimaopnlem  25631  itg1addlem4  25675  dvcmul  25920  dvcmulf  25921  dvexp  25929  c1liplem1  25973  deg1n0ima  26066  pserulm  26402  psercn2  26403  psercn2OLD  26404  psercnlem2  26405  psercnlem1  26406  psercn  26407  pserdvlem1  26408  pserdvlem2  26409  pserdv  26410  pserdv2  26411  abelth  26422  efcn  26424  efcvx  26430  eff1olem  26528  dvrelog  26617  logf1o2  26630  dvlog  26631  efopn  26638  logtayl  26640  cxpcn3lem  26728  cxpcn3  26729  resqrtcn  26730  atancl  26862  atanval  26865  dvatan  26916  atancn  26917  bdaydm  27761  lltr  27873  madess  27877  oldssmade  27878  oldss  27881  madebdayim  27899  oldbdayim  27900  lrold  27908  madefi  27924  oldfi  27925  cutminmax  27947  oldfib  28388  topnfbey  30559  cnaddabloOLD  30672  cnidOLD  30673  cncvcOLD  30674  cnnv  30768  cnnvba  30770  cncph  30910  dfhnorm2  31213  hilablo  31251  hilid  31252  hilvc  31253  hhnv  31256  hhba  31258  hhph  31269  issh2  31300  hhssabloi  31353  hhssnv  31355  hhshsslem1  31358  imaelshi  32149  rnelshi  32150  nlelshi  32151  xrofsup  32860  ply1degltel  33674  ply1degleel  33675  ply1degltlss  33676  coinfliprv  34648  erdszelem2  35395  erdszelem5  35398  erdszelem8  35401  msrrcl  35746  mthmsta  35781  icoreunrn  37686  icoreelrn  37688  relowlpssretop  37691  poimirlem26  37978  poimirlem27  37979  opnmbllem0  37988  dvtan  38002  fpwfvss  43854  seff  44751  sblpnf  44752  dvsconst  44772  dvsid  44773  dvsef  44774  expgrowth  44777  binomcxplemdvbinom  44795  binomcxplemdvsum  44797  binomcxplemnotnn0  44798  addcomgi  44897  dmuz  45678  dmico  46008  dvsinax  46356  fvvolioof  46432  fvvolicof  46434  dirkercncflem2  46547  fourierdlem42  46592  hoicvr  46991  ovolval3  47090  sinnpoly  47336  fucofvalne  49797