Theorem fdmi 6709

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

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5647  ⟶wf 6523

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6530  df-f 6531

This theorem is used by:  f0cli  7086  rankvaln  9781  isnum2  9998  r0weon  10063  cfub  10298  cardcf  10301  cflecard  10302  cfle  10303  cflim2  10313  cfidm  10325  cardf  10606  smobeth  10643  inar1  10832  addcompq  11007  addcomnq  11008  mulcompq  11009  mulcomnq  11010  adderpq  11013  mulerpq  11014  addassnq  11015  mulassnq  11016  distrnq  11018  recmulnq  11021  recclnq  11023  dmrecnq  11025  lterpq  11027  ltanq  11028  ltmnq  11029  ltexnq  11032  nsmallnq  11034  ltbtwnnq  11035  prlem934  11090  ltaddpr  11091  ltexprlem2  11094  ltexprlem3  11095  ltexprlem4  11096  ltexprlem6  11098  ltexprlem7  11099  prlem936  11104  eluzel2  12940  uzssz  12956  elixx3g  13459  ndmioo  13473  elfz2  13616  fz0  13641  elfzoel1  13760  elfzoel2  13761  fzoval  13763  ltweuz  14073  fzofi  14086  dmhashres  14453  s1dm  14723  s2dm  15009  sumz  15856  sumss  15858  prod1  16079  prodss  16082  znnen  16348  unbenlem  17048  prmreclem6  17061  eldmcoa  18202  efgsdm  19906  efgsval  19907  efgsp1  19913  efgsfo  19915  efgredleme  19919  efgred  19924  gexex  20029  torsubg  20030  dmdprd  20176  dprdval  20181  iocpnfordt  23495  icomnfordt  23496  uzrest  24178  qtopbaslem  25039  retopbas  25041  tgqioo  25081  re2ndc  25082  bndth  25241  tcphcph  25520  ovolficcss  25752  ismbl  25809  uniiccdif  25861  dyadmbllem  25882  opnmbllem  25884  opnmblALT  25886  mbfimaopnlem  25938  itg1addlem4  25982  dvcmul  26226  dvcmulf  26227  dvexp  26235  c1liplem1  26278  deg1n0ima  26369  pserulm  26713  psercn2  26714  psercnlem2  26715  psercnlem1  26716  psercn  26717  pserdvlem1  26718  pserdvlem2  26719  pserdv  26720  pserdv2  26721  abelth  26732  efcn  26734  efcvx  26740  eff1olem  26840  dvrelog  26929  logf1o2  26942  dvlog  26943  efopn  26950  logtayl  26952  cxpcn3lem  27039  cxpcn3  27040  resqrtcn  27041  atancl  27173  atanval  27176  dvatan  27227  atancn  27228  bdaydmOLD  28070  lltr  28182  madess  28186  oldssmade  28187  oldss  28190  madebdayim  28208  oldbdayim  28209  lrold  28217  madefi  28233  oldfi  28234  cutminmax  28256  oldfib  28697  topnfbey  31004  cnaddabloOLD  31117  cnidOLD  31118  cncvcOLD  31119  cnnv  31213  cnnvba  31215  cncph  31355  dfhnorm2  31658  hilablo  31696  hilid  31697  hilvc  31698  hhnv  31701  hhba  31703  hhph  31714  issh2  31745  hhssabloi  31798  hhssnv  31800  hhshsslem1  31803  imaelshi  32594  rnelshi  32595  nlelshi  32596  xrofsup  33293  ply1degltel  34060  ply1degleel  34061  ply1degltlss  34062  coinfliprv  35050  dfscott3  35673  erdszelem2  35878  erdszelem5  35881  erdszelem8  35884  msrrcl  36229  mthmsta  36264  icoreunrn  38202  icoreelrn  38204  relowlpssretop  38207  poimirlem26  38484  poimirlem27  38485  opnmbllem0  38494  dvtan  38508  fpwfvss  44356  seff  45237  sblpnf  45238  dvsconst  45258  dvsid  45259  dvsef  45260  expgrowth  45263  binomcxplemdvbinom  45281  binomcxplemdvsum  45283  binomcxplemnotnn0  45284  addcomgi  45382  dmuz  46167  dmico  46497  dvsinax  46845  fvvolioof  46921  fvvolicof  46923  dirkercncflem2  47036  fourierdlem42  47081  hoicvr  47480  ovolval3  47579  tannpoly  47862  sinnpoly  47863  fucofvalne  50355  dvsec  50778  dvcsc  50779  dvcot  50780