Theorem fdmi 6692

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

Syntax hints:   = wceq 1554  dom cdm 5640  ⟶wf 6506

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 209  df-an 399  df-fn 6513  df-f 6514

This theorem is referenced by:  f0cli  7068  rankvaln  9747  isnum2  9893  r0weon  9958  cfub  10195  cardcf  10198  cflecard  10199  cfle  10200  cflim2  10210  cfidm  10222  cardf  10497  smobeth  10534  inar1  10723  addcompq  10898  addcomnq  10899  mulcompq  10900  mulcomnq  10901  adderpq  10904  mulerpq  10905  addassnq  10906  mulassnq  10907  distrnq  10909  recmulnq  10912  recclnq  10914  dmrecnq  10916  lterpq  10918  ltanq  10919  ltmnq  10920  ltexnq  10923  nsmallnq  10925  ltbtwnnq  10926  prlem934  10981  ltaddpr  10982  ltexprlem2  10985  ltexprlem3  10986  ltexprlem4  10987  ltexprlem6  10989  ltexprlem7  10990  prlem936  10995  eluzel2  12834  uzssz  12850  elixx3g  13352  ndmioo  13366  elfz2  13509  fz0  13534  elfzoel1  13652  elfzoel2  13653  fzoval  13655  ltweuz  13964  fzofi  13977  dmhashres  14344  s1dm  14612  s2dm  14893  sumz  15725  sumss  15727  prod1  15950  prodss  15953  znnen  16220  unbenlem  16920  prmreclem6  16933  eldmcoa  18074  efgsdm  19746  efgsval  19747  efgsp1  19753  efgsfo  19755  efgredleme  19759  efgred  19764  gexex  19869  torsubg  19870  dmdprd  20016  dprdval  20021  iocpnfordt  23248  icomnfordt  23249  uzrest  23930  qtopbaslem  24791  retopbas  24793  tgqioo  24833  re2ndc  24834  bndth  24993  tcphcph  25272  ovolficcss  25504  ismbl  25561  uniiccdif  25613  dyadmbllem  25634  opnmbllem  25636  opnmblALT  25638  mbfimaopnlem  25690  itg1addlem4  25734  dvcmul  25979  dvcmulf  25980  dvexp  25988  c1liplem1  26031  deg1n0ima  26122  pserulm  26455  psercn2  26456  psercnlem2  26457  psercnlem1  26458  psercn  26459  pserdvlem1  26460  pserdvlem2  26461  pserdv  26462  pserdv2  26463  abelth  26474  efcn  26476  efcvx  26482  eff1olem  26583  dvrelog  26672  logf1o2  26685  dvlog  26686  efopn  26693  logtayl  26695  cxpcn3lem  26782  cxpcn3  26783  resqrtcn  26784  atancl  26916  atanval  26919  dvatan  26970  atancn  26971  bdaydmOLD  27813  lltr  27925  madess  27929  oldssmade  27930  oldss  27933  madebdayim  27951  oldbdayim  27952  lrold  27960  madefi  27976  oldfi  27977  cutminmax  27999  oldfib  28440  topnfbey  30610  cnaddabloOLD  30723  cnidOLD  30724  cncvcOLD  30725  cnnv  30819  cnnvba  30821  cncph  30961  dfhnorm2  31264  hilablo  31302  hilid  31303  hilvc  31304  hhnv  31307  hhba  31309  hhph  31320  issh2  31351  hhssabloi  31404  hhssnv  31406  hhshsslem1  31409  imaelshi  32200  rnelshi  32201  nlelshi  32202  xrofsup  32912  ply1degltel  33744  ply1degleel  33745  ply1degltlss  33746  coinfliprv  34734  erdszelem2  35490  erdszelem5  35493  erdszelem8  35496  msrrcl  35841  mthmsta  35876  icoreunrn  37801  icoreelrn  37803  relowlpssretop  37806  poimirlem26  38093  poimirlem27  38094  opnmbllem0  38103  dvtan  38117  fpwfvss  43936  seff  44833  sblpnf  44834  dvsconst  44854  dvsid  44855  dvsef  44856  expgrowth  44859  binomcxplemdvbinom  44877  binomcxplemdvsum  44879  binomcxplemnotnn0  44880  addcomgi  44979  dmuz  45757  dmico  46087  dvsinax  46435  fvvolioof  46511  fvvolicof  46513  dirkercncflem2  46626  fourierdlem42  46671  hoicvr  47070  ovolval3  47169  sinnpoly  47433  fucofvalne  49894