Theorem fdmi 6758

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

Syntax hints:   = wceq 1537  dom cdm 5700  ⟶wf 6569

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 6576  df-f 6577

This theorem is referenced by:  f0cli  7132  rankvaln  9868  isnum2  10014  r0weon  10081  cfub  10318  cardcf  10321  cflecard  10322  cfle  10323  cflim2  10332  cfidm  10344  cardf  10619  smobeth  10655  inar1  10844  addcompq  11019  addcomnq  11020  mulcompq  11021  mulcomnq  11022  adderpq  11025  mulerpq  11026  addassnq  11027  mulassnq  11028  distrnq  11030  recmulnq  11033  recclnq  11035  dmrecnq  11037  lterpq  11039  ltanq  11040  ltmnq  11041  ltexnq  11044  nsmallnq  11046  ltbtwnnq  11047  prlem934  11102  ltaddpr  11103  ltexprlem2  11106  ltexprlem3  11107  ltexprlem4  11108  ltexprlem6  11110  ltexprlem7  11111  prlem936  11116  eluzel2  12908  uzssz  12924  elixx3g  13420  ndmioo  13434  elfz2  13574  fz0  13599  elfzoel1  13714  elfzoel2  13715  fzoval  13717  ltweuz  14012  fzofi  14025  dmhashres  14390  s1dm  14656  s2dm  14939  sumz  15770  sumss  15772  prod1  15992  prodss  15995  znnen  16260  unbenlem  16955  prmreclem6  16968  eldmcoa  18132  efgsdm  19772  efgsval  19773  efgsp1  19779  efgsfo  19781  efgredleme  19785  efgred  19790  gexex  19895  torsubg  19896  dmdprd  20042  dprdval  20047  iocpnfordt  23244  icomnfordt  23245  uzrest  23926  qtopbaslem  24800  retopbas  24802  tgqioo  24841  re2ndc  24842  bndth  25009  tcphcph  25290  ovolficcss  25523  ismbl  25580  uniiccdif  25632  dyadmbllem  25653  opnmbllem  25655  opnmblALT  25657  mbfimaopnlem  25709  itg1addlem4  25753  itg1addlem4OLD  25754  dvcmul  26001  dvcmulf  26002  dvexp  26011  c1liplem1  26055  deg1n0ima  26148  pserulm  26483  psercn2  26484  psercn2OLD  26485  psercnlem2  26486  psercnlem1  26487  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  pserdv  26491  pserdv2  26492  abelth  26503  efcn  26505  efcvx  26511  eff1olem  26608  dvrelog  26697  logf1o2  26710  dvlog  26711  efopn  26718  logtayl  26720  cxpcn3lem  26808  cxpcn3  26809  resqrtcn  26810  atancl  26942  atanval  26945  dvatan  26996  atancn  26997  bdaydm  27837  lltropt  27929  madess  27933  oldssmade  27934  madebdayim  27944  oldbdayim  27945  lrold  27953  madefi  27968  oldfi  27969  topnfbey  30501  cnaddabloOLD  30613  cnidOLD  30614  cncvcOLD  30615  cnnv  30709  cnnvba  30711  cncph  30851  dfhnorm2  31154  hilablo  31192  hilid  31193  hilvc  31194  hhnv  31197  hhba  31199  hhph  31210  issh2  31241  hhssabloi  31294  hhssnv  31296  hhshsslem1  31299  imaelshi  32090  rnelshi  32091  nlelshi  32092  xrofsup  32774  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  coinfliprv  34447  erdszelem2  35160  erdszelem5  35163  erdszelem8  35166  msrrcl  35511  mthmsta  35546  icoreunrn  37325  icoreelrn  37327  relowlpssretop  37330  poimirlem26  37606  poimirlem27  37607  opnmbllem0  37616  dvtan  37630  fpwfvss  43374  seff  44278  sblpnf  44279  dvsconst  44299  dvsid  44300  dvsef  44301  expgrowth  44304  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  addcomgi  44425  dmuz  45141  dmico  45483  dvsinax  45834  fvvolioof  45910  fvvolicof  45912  dirkercncflem2  46025  fourierdlem42  46070  hoicvr  46469  ovolval3  46568