Theorem fdmi 6716

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

Syntax hints:   = wceq 1540  dom cdm 5654  ⟶wf 6526

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 6533  df-f 6534

This theorem is referenced by:  f0cli  7087  rankvaln  9811  isnum2  9957  r0weon  10024  cfub  10261  cardcf  10264  cflecard  10265  cfle  10266  cflim2  10275  cfidm  10287  cardf  10562  smobeth  10598  inar1  10787  addcompq  10962  addcomnq  10963  mulcompq  10964  mulcomnq  10965  adderpq  10968  mulerpq  10969  addassnq  10970  mulassnq  10971  distrnq  10973  recmulnq  10976  recclnq  10978  dmrecnq  10980  lterpq  10982  ltanq  10983  ltmnq  10984  ltexnq  10987  nsmallnq  10989  ltbtwnnq  10990  prlem934  11045  ltaddpr  11046  ltexprlem2  11049  ltexprlem3  11050  ltexprlem4  11051  ltexprlem6  11053  ltexprlem7  11054  prlem936  11059  eluzel2  12855  uzssz  12871  elixx3g  13373  ndmioo  13387  elfz2  13529  fz0  13554  elfzoel1  13672  elfzoel2  13673  fzoval  13675  ltweuz  13977  fzofi  13990  dmhashres  14357  s1dm  14624  s2dm  14907  sumz  15736  sumss  15738  prod1  15958  prodss  15961  znnen  16228  unbenlem  16926  prmreclem6  16939  eldmcoa  18076  efgsdm  19709  efgsval  19710  efgsp1  19716  efgsfo  19718  efgredleme  19722  efgred  19727  gexex  19832  torsubg  19833  dmdprd  19979  dprdval  19984  iocpnfordt  23151  icomnfordt  23152  uzrest  23833  qtopbaslem  24695  retopbas  24697  tgqioo  24737  re2ndc  24738  bndth  24906  tcphcph  25187  ovolficcss  25420  ismbl  25477  uniiccdif  25529  dyadmbllem  25550  opnmbllem  25552  opnmblALT  25554  mbfimaopnlem  25606  itg1addlem4  25650  dvcmul  25897  dvcmulf  25898  dvexp  25907  c1liplem1  25951  deg1n0ima  26044  pserulm  26381  psercn2  26382  psercn2OLD  26383  psercnlem2  26384  psercnlem1  26385  psercn  26386  pserdvlem1  26387  pserdvlem2  26388  pserdv  26389  pserdv2  26390  abelth  26401  efcn  26403  efcvx  26409  eff1olem  26507  dvrelog  26596  logf1o2  26609  dvlog  26610  efopn  26617  logtayl  26619  cxpcn3lem  26707  cxpcn3  26708  resqrtcn  26709  atancl  26841  atanval  26844  dvatan  26895  atancn  26896  bdaydm  27736  lltropt  27828  madess  27832  oldssmade  27833  madebdayim  27843  oldbdayim  27844  lrold  27852  madefi  27867  oldfi  27868  topnfbey  30396  cnaddabloOLD  30508  cnidOLD  30509  cncvcOLD  30510  cnnv  30604  cnnvba  30606  cncph  30746  dfhnorm2  31049  hilablo  31087  hilid  31088  hilvc  31089  hhnv  31092  hhba  31094  hhph  31105  issh2  31136  hhssabloi  31189  hhssnv  31191  hhshsslem1  31194  imaelshi  31985  rnelshi  31986  nlelshi  31987  xrofsup  32690  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  coinfliprv  34461  erdszelem2  35160  erdszelem5  35163  erdszelem8  35166  msrrcl  35511  mthmsta  35546  icoreunrn  37323  icoreelrn  37325  relowlpssretop  37328  poimirlem26  37616  poimirlem27  37617  opnmbllem0  37626  dvtan  37640  fpwfvss  43383  seff  44281  sblpnf  44282  dvsconst  44302  dvsid  44303  dvsef  44304  expgrowth  44307  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  addcomgi  44428  dmuz  45206  dmico  45540  dvsinax  45890  fvvolioof  45966  fvvolicof  45968  dirkercncflem2  46081  fourierdlem42  46126  hoicvr  46525  ovolval3  46624  fucofvalne  49184