Theorem fdmi 6747

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

Syntax hints:   = wceq 1540  dom cdm 5685  ⟶wf 6557

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 6564  df-f 6565

This theorem is referenced by:  f0cli  7118  rankvaln  9839  isnum2  9985  r0weon  10052  cfub  10289  cardcf  10292  cflecard  10293  cfle  10294  cflim2  10303  cfidm  10315  cardf  10590  smobeth  10626  inar1  10815  addcompq  10990  addcomnq  10991  mulcompq  10992  mulcomnq  10993  adderpq  10996  mulerpq  10997  addassnq  10998  mulassnq  10999  distrnq  11001  recmulnq  11004  recclnq  11006  dmrecnq  11008  lterpq  11010  ltanq  11011  ltmnq  11012  ltexnq  11015  nsmallnq  11017  ltbtwnnq  11018  prlem934  11073  ltaddpr  11074  ltexprlem2  11077  ltexprlem3  11078  ltexprlem4  11079  ltexprlem6  11081  ltexprlem7  11082  prlem936  11087  eluzel2  12883  uzssz  12899  elixx3g  13400  ndmioo  13414  elfz2  13554  fz0  13579  elfzoel1  13697  elfzoel2  13698  fzoval  13700  ltweuz  14002  fzofi  14015  dmhashres  14380  s1dm  14646  s2dm  14929  sumz  15758  sumss  15760  prod1  15980  prodss  15983  znnen  16248  unbenlem  16946  prmreclem6  16959  eldmcoa  18110  efgsdm  19748  efgsval  19749  efgsp1  19755  efgsfo  19757  efgredleme  19761  efgred  19766  gexex  19871  torsubg  19872  dmdprd  20018  dprdval  20023  iocpnfordt  23223  icomnfordt  23224  uzrest  23905  qtopbaslem  24779  retopbas  24781  tgqioo  24821  re2ndc  24822  bndth  24990  tcphcph  25271  ovolficcss  25504  ismbl  25561  uniiccdif  25613  dyadmbllem  25634  opnmbllem  25636  opnmblALT  25638  mbfimaopnlem  25690  itg1addlem4  25734  dvcmul  25981  dvcmulf  25982  dvexp  25991  c1liplem1  26035  deg1n0ima  26128  pserulm  26465  psercn2  26466  psercn2OLD  26467  psercnlem2  26468  psercnlem1  26469  psercn  26470  pserdvlem1  26471  pserdvlem2  26472  pserdv  26473  pserdv2  26474  abelth  26485  efcn  26487  efcvx  26493  eff1olem  26590  dvrelog  26679  logf1o2  26692  dvlog  26693  efopn  26700  logtayl  26702  cxpcn3lem  26790  cxpcn3  26791  resqrtcn  26792  atancl  26924  atanval  26927  dvatan  26978  atancn  26979  bdaydm  27819  lltropt  27911  madess  27915  oldssmade  27916  madebdayim  27926  oldbdayim  27927  lrold  27935  madefi  27950  oldfi  27951  topnfbey  30488  cnaddabloOLD  30600  cnidOLD  30601  cncvcOLD  30602  cnnv  30696  cnnvba  30698  cncph  30838  dfhnorm2  31141  hilablo  31179  hilid  31180  hilvc  31181  hhnv  31184  hhba  31186  hhph  31197  issh2  31228  hhssabloi  31281  hhssnv  31283  hhshsslem1  31286  imaelshi  32077  rnelshi  32078  nlelshi  32079  xrofsup  32771  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  coinfliprv  34485  erdszelem2  35197  erdszelem5  35200  erdszelem8  35203  msrrcl  35548  mthmsta  35583  icoreunrn  37360  icoreelrn  37362  relowlpssretop  37365  poimirlem26  37653  poimirlem27  37654  opnmbllem0  37663  dvtan  37677  fpwfvss  43425  seff  44328  sblpnf  44329  dvsconst  44349  dvsid  44350  dvsef  44351  expgrowth  44354  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  addcomgi  44475  dmuz  45239  dmico  45578  dvsinax  45928  fvvolioof  46004  fvvolicof  46006  dirkercncflem2  46119  fourierdlem42  46164  hoicvr  46563  ovolval3  46662  fucofvalne  49020