Theorem fdmi 6681

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

Syntax hints:   = wceq 1542  dom cdm 5632  ⟶wf 6496

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 6503  df-f 6504

This theorem is referenced by:  f0cli  7052  rankvaln  9723  isnum2  9869  r0weon  9934  cfub  10171  cardcf  10174  cflecard  10175  cfle  10176  cflim2  10185  cfidm  10197  cardf  10472  smobeth  10509  inar1  10698  addcompq  10873  addcomnq  10874  mulcompq  10875  mulcomnq  10876  adderpq  10879  mulerpq  10880  addassnq  10881  mulassnq  10882  distrnq  10884  recmulnq  10887  recclnq  10889  dmrecnq  10891  lterpq  10893  ltanq  10894  ltmnq  10895  ltexnq  10898  nsmallnq  10900  ltbtwnnq  10901  prlem934  10956  ltaddpr  10957  ltexprlem2  10960  ltexprlem3  10961  ltexprlem4  10962  ltexprlem6  10964  ltexprlem7  10965  prlem936  10970  eluzel2  12768  uzssz  12784  elixx3g  13286  ndmioo  13300  elfz2  13442  fz0  13467  elfzoel1  13585  elfzoel2  13586  fzoval  13588  ltweuz  13896  fzofi  13909  dmhashres  14276  s1dm  14544  s2dm  14825  sumz  15657  sumss  15659  prod1  15879  prodss  15882  znnen  16149  unbenlem  16848  prmreclem6  16861  eldmcoa  18001  efgsdm  19671  efgsval  19672  efgsp1  19678  efgsfo  19680  efgredleme  19684  efgred  19689  gexex  19794  torsubg  19795  dmdprd  19941  dprdval  19946  iocpnfordt  23171  icomnfordt  23172  uzrest  23853  qtopbaslem  24714  retopbas  24716  tgqioo  24756  re2ndc  24757  bndth  24925  tcphcph  25205  ovolficcss  25438  ismbl  25495  uniiccdif  25547  dyadmbllem  25568  opnmbllem  25570  opnmblALT  25572  mbfimaopnlem  25624  itg1addlem4  25668  dvcmul  25915  dvcmulf  25916  dvexp  25925  c1liplem1  25969  deg1n0ima  26062  pserulm  26399  psercn2  26400  psercn2OLD  26401  psercnlem2  26402  psercnlem1  26403  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  pserdv  26407  pserdv2  26408  abelth  26419  efcn  26421  efcvx  26427  eff1olem  26525  dvrelog  26614  logf1o2  26627  dvlog  26628  efopn  26635  logtayl  26637  cxpcn3lem  26725  cxpcn3  26726  resqrtcn  26727  atancl  26859  atanval  26862  dvatan  26913  atancn  26914  bdaydm  27758  lltr  27870  madess  27874  oldssmade  27875  oldss  27878  madebdayim  27896  oldbdayim  27897  lrold  27905  madefi  27921  oldfi  27922  cutminmax  27944  oldfib  28385  topnfbey  30556  cnaddabloOLD  30668  cnidOLD  30669  cncvcOLD  30670  cnnv  30764  cnnvba  30766  cncph  30906  dfhnorm2  31209  hilablo  31247  hilid  31248  hilvc  31249  hhnv  31252  hhba  31254  hhph  31265  issh2  31296  hhssabloi  31349  hhssnv  31351  hhshsslem1  31354  imaelshi  32145  rnelshi  32146  nlelshi  32147  xrofsup  32857  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  coinfliprv  34660  erdszelem2  35405  erdszelem5  35408  erdszelem8  35411  msrrcl  35756  mthmsta  35791  icoreunrn  37603  icoreelrn  37605  relowlpssretop  37608  poimirlem26  37886  poimirlem27  37887  opnmbllem0  37896  dvtan  37910  fpwfvss  43757  seff  44654  sblpnf  44655  dvsconst  44675  dvsid  44676  dvsef  44677  expgrowth  44680  binomcxplemdvbinom  44698  binomcxplemdvsum  44700  binomcxplemnotnn0  44701  addcomgi  44800  dmuz  45581  dmico  45912  dvsinax  46260  fvvolioof  46336  fvvolicof  46338  dirkercncflem2  46451  fourierdlem42  46496  hoicvr  46895  ovolval3  46994  sinnpoly  47240  fucofvalne  49673