Theorem fdmi 6201

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

Syntax hints:   = wceq 1620  dom cdm 5254  ⟶wf 6033

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 197  df-an 385  df-fn 6040  df-f 6041

This theorem is referenced by:  f0cli  6521  rankvaln  8823  isnum2  8932  r0weon  8996  cfub  9234  cardcf  9237  cflecard  9238  cfle  9239  cflim2  9248  cfidm  9260  cardf  9535  smobeth  9571  inar1  9760  addcompq  9935  addcomnq  9936  mulcompq  9937  mulcomnq  9938  adderpq  9941  mulerpq  9942  addassnq  9943  mulassnq  9944  distrnq  9946  recmulnq  9949  recclnq  9951  dmrecnq  9953  lterpq  9955  ltanq  9956  ltmnq  9957  ltexnq  9960  nsmallnq  9962  ltbtwnnq  9963  prlem934  10018  ltaddpr  10019  ltexprlem2  10022  ltexprlem3  10023  ltexprlem4  10024  ltexprlem6  10026  ltexprlem7  10027  prlem936  10032  eluzel2  11855  uzssz  11870  elixx3g  12352  ndmioo  12366  elfz2  12497  fz0  12520  elfzoel1  12633  elfzoel2  12634  fzoval  12636  ltweuz  12925  fzofi  12938  dmhashres  13294  s1dm  13550  s2dm  13806  sumz  14623  sumss  14625  prod1  14844  prodss  14847  znnen  15111  unbenlem  15785  prmreclem6  15798  eldmcoa  16887  efgsdm  18314  efgsval  18315  efgsp1  18321  efgsfo  18323  efgredleme  18327  efgred  18332  gexex  18427  torsubg  18428  dmdprd  18568  dprdval  18573  iocpnfordt  21192  icomnfordt  21193  uzrest  21873  qtopbaslem  22734  retopbas  22736  tgqioo  22775  re2ndc  22776  bndth  22929  tchcph  23207  ovolficcss  23409  ismbl  23465  uniiccdif  23517  dyadmbllem  23538  opnmbllem  23540  opnmblALT  23542  mbfimaopnlem  23592  itg1addlem4  23636  dvcmul  23877  dvcmulf  23878  dvexp  23886  c1liplem1  23929  deg1n0ima  24019  pserulm  24346  psercn2  24347  psercnlem2  24348  psercnlem1  24349  psercn  24350  pserdvlem1  24351  pserdvlem2  24352  pserdv  24353  pserdv2  24354  abelth  24365  efcn  24367  efcvx  24373  eff1olem  24464  dvrelog  24553  logf1o2  24566  dvlog  24567  efopn  24574  logtayl  24576  cxpcn3lem  24658  cxpcn3  24659  resqrtcn  24660  atancl  24778  atanval  24781  dvatan  24832  atancn  24833  topnfbey  27607  cnaddabloOLD  27716  cnidOLD  27717  cncvcOLD  27718  cnnv  27812  cnnvba  27814  cncph  27954  dfhnorm2  28259  hilablo  28297  hilid  28298  hilvc  28299  hhnv  28302  hhba  28304  hhph  28315  issh2  28346  hhssabloi  28399  hhssnv  28401  hhshsslem1  28404  imaelshi  29197  rnelshi  29198  nlelshi  29199  xrofsup  29813  coinfliprv  30824  erdszelem2  31452  erdszelem5  31455  erdszelem8  31458  msrrcl  31718  mthmsta  31753  bdaydm  32167  icoreunrn  33489  icoreelrn  33491  relowlpssretop  33494  poimirlem26  33717  poimirlem27  33718  opnmbllem0  33727  dvtan  33742  seff  38979  sblpnf  38980  dvsconst  39000  dvsid  39001  dvsef  39002  expgrowth  39005  binomcxplemdvbinom  39023  binomcxplemdvsum  39025  binomcxplemnotnn0  39026  addcomgi  39131  dmuz  39908  dmico  40264  dvsinax  40599  fvvolioof  40678  fvvolicof  40680  dirkercncflem2  40793  fourierdlem42  40838  hoicvr  41237  ovolval3  41336