Theorem fdmi 6718

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

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5659  ⟶wf 6533

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 6540  df-f 6541

This theorem is used by:  f0cli  7094  rankvaln  9784  isnum2  9953  r0weon  10018  cfub  10253  cardcf  10256  cflecard  10257  cfle  10258  cflim2  10268  cfidm  10280  cardf  10561  smobeth  10598  inar1  10787  addcompq  10962  addcomnq  10963  mulcompq  10964  mulcomnq  10965  adderpq  10968  mulerpq  10969  addassnq  10970  mulassnq  10971  distrnq  10973  recmulnq  10976  recclnq  10978  dmrecnq  10980  lterpq  10982  ltanq  10983  ltmnq  10984  ltexnq  10987  nsmallnq  10989  ltbtwnnq  10990  prlem934  11045  ltaddpr  11046  ltexprlem2  11049  ltexprlem3  11050  ltexprlem4  11051  ltexprlem6  11053  ltexprlem7  11054  prlem936  11059  eluzel2  12895  uzssz  12911  elixx3g  13413  ndmioo  13427  elfz2  13570  fz0  13595  elfzoel1  13714  elfzoel2  13715  fzoval  13717  ltweuz  14027  fzofi  14040  dmhashres  14407  s1dm  14677  s2dm  14963  sumz  15810  sumss  15812  prod1  16035  prodss  16038  znnen  16304  unbenlem  17004  prmreclem6  17017  eldmcoa  18158  efgsdm  19861  efgsval  19862  efgsp1  19868  efgsfo  19870  efgredleme  19874  efgred  19879  gexex  19984  torsubg  19985  dmdprd  20131  dprdval  20136  iocpnfordt  23444  icomnfordt  23445  uzrest  24127  qtopbaslem  24988  retopbas  24990  tgqioo  25030  re2ndc  25031  bndth  25190  tcphcph  25469  ovolficcss  25701  ismbl  25758  uniiccdif  25810  dyadmbllem  25831  opnmbllem  25833  opnmblALT  25835  mbfimaopnlem  25887  itg1addlem4  25931  dvcmul  26176  dvcmulf  26177  dvexp  26185  c1liplem1  26228  deg1n0ima  26319  pserulm  26658  psercn2  26659  psercnlem2  26660  psercnlem1  26661  psercn  26662  pserdvlem1  26663  pserdvlem2  26664  pserdv  26665  pserdv2  26666  abelth  26677  efcn  26679  efcvx  26685  eff1olem  26786  dvrelog  26875  logf1o2  26888  dvlog  26889  efopn  26896  logtayl  26898  cxpcn3lem  26985  cxpcn3  26986  resqrtcn  26987  atancl  27119  atanval  27122  dvatan  27173  atancn  27174  bdaydmOLD  28016  lltr  28128  madess  28132  oldssmade  28133  oldss  28136  madebdayim  28154  oldbdayim  28155  lrold  28163  madefi  28179  oldfi  28180  cutminmax  28202  oldfib  28643  topnfbey  30950  cnaddabloOLD  31063  cnidOLD  31064  cncvcOLD  31065  cnnv  31159  cnnvba  31161  cncph  31301  dfhnorm2  31604  hilablo  31642  hilid  31643  hilvc  31644  hhnv  31647  hhba  31649  hhph  31660  issh2  31691  hhssabloi  31744  hhssnv  31746  hhshsslem1  31749  imaelshi  32540  rnelshi  32541  nlelshi  32542  xrofsup  33240  ply1degltel  34006  ply1degleel  34007  ply1degltlss  34008  coinfliprv  34996  dfscott3  35628  erdszelem2  35773  erdszelem5  35776  erdszelem8  35779  msrrcl  36124  mthmsta  36159  icoreunrn  38115  icoreelrn  38117  relowlpssretop  38120  poimirlem26  38397  poimirlem27  38398  opnmbllem0  38407  dvtan  38421  fpwfvss  44254  seff  45135  sblpnf  45136  dvsconst  45156  dvsid  45157  dvsef  45158  expgrowth  45161  binomcxplemdvbinom  45179  binomcxplemdvsum  45181  binomcxplemnotnn0  45182  addcomgi  45280  dmuz  46065  dmico  46395  dvsinax  46743  fvvolioof  46819  fvvolicof  46821  dirkercncflem2  46934  fourierdlem42  46979  hoicvr  47378  ovolval3  47477  tannpoly  47760  sinnpoly  47761  fucofvalne  50253  dvsec  50691  dvcsc  50692  dvcot  50693