Theorem fdmi 6596

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

Syntax hints:   = wceq 1539  dom cdm 5580  ⟶wf 6414

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 206  df-an 396  df-fn 6421  df-f 6422

This theorem is referenced by:  f0cli  6956  rankvaln  9488  isnum2  9634  r0weon  9699  cfub  9936  cardcf  9939  cflecard  9940  cfle  9941  cflim2  9950  cfidm  9962  cardf  10237  smobeth  10273  inar1  10462  addcompq  10637  addcomnq  10638  mulcompq  10639  mulcomnq  10640  adderpq  10643  mulerpq  10644  addassnq  10645  mulassnq  10646  distrnq  10648  recmulnq  10651  recclnq  10653  dmrecnq  10655  lterpq  10657  ltanq  10658  ltmnq  10659  ltexnq  10662  nsmallnq  10664  ltbtwnnq  10665  prlem934  10720  ltaddpr  10721  ltexprlem2  10724  ltexprlem3  10725  ltexprlem4  10726  ltexprlem6  10728  ltexprlem7  10729  prlem936  10734  eluzel2  12516  uzssz  12532  elixx3g  13021  ndmioo  13035  elfz2  13175  fz0  13200  elfzoel1  13314  elfzoel2  13315  fzoval  13317  ltweuz  13609  fzofi  13622  dmhashres  13983  s1dm  14241  s2dm  14531  sumz  15362  sumss  15364  prod1  15582  prodss  15585  znnen  15849  unbenlem  16537  prmreclem6  16550  eldmcoa  17696  efgsdm  19251  efgsval  19252  efgsp1  19258  efgsfo  19260  efgredleme  19264  efgred  19269  gexex  19369  torsubg  19370  dmdprd  19516  dprdval  19521  iocpnfordt  22274  icomnfordt  22275  uzrest  22956  qtopbaslem  23828  retopbas  23830  tgqioo  23869  re2ndc  23870  bndth  24027  tcphcph  24306  ovolficcss  24538  ismbl  24595  uniiccdif  24647  dyadmbllem  24668  opnmbllem  24670  opnmblALT  24672  mbfimaopnlem  24724  itg1addlem4  24768  itg1addlem4OLD  24769  dvcmul  25013  dvcmulf  25014  dvexp  25022  c1liplem1  25065  deg1n0ima  25159  pserulm  25486  psercn2  25487  psercnlem2  25488  psercnlem1  25489  psercn  25490  pserdvlem1  25491  pserdvlem2  25492  pserdv  25493  pserdv2  25494  abelth  25505  efcn  25507  efcvx  25513  eff1olem  25609  dvrelog  25697  logf1o2  25710  dvlog  25711  efopn  25718  logtayl  25720  cxpcn3lem  25805  cxpcn3  25806  resqrtcn  25807  atancl  25936  atanval  25939  dvatan  25990  atancn  25991  topnfbey  28734  cnaddabloOLD  28844  cnidOLD  28845  cncvcOLD  28846  cnnv  28940  cnnvba  28942  cncph  29082  dfhnorm2  29385  hilablo  29423  hilid  29424  hilvc  29425  hhnv  29428  hhba  29430  hhph  29441  issh2  29472  hhssabloi  29525  hhssnv  29527  hhshsslem1  29530  imaelshi  30321  rnelshi  30322  nlelshi  30323  xrofsup  30992  coinfliprv  32349  erdszelem2  33054  erdszelem5  33057  erdszelem8  33060  msrrcl  33405  mthmsta  33440  bdaydm  33896  madess  33986  oldssmade  33987  madebdayim  33997  oldbdayim  33998  lrold  34004  icoreunrn  35457  icoreelrn  35459  relowlpssretop  35462  poimirlem26  35730  poimirlem27  35731  opnmbllem0  35740  dvtan  35754  seff  41816  sblpnf  41817  dvsconst  41837  dvsid  41838  dvsef  41839  expgrowth  41842  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  addcomgi  41963  dmuz  42666  dmico  42993  dvsinax  43344  fvvolioof  43420  fvvolicof  43422  dirkercncflem2  43535  fourierdlem42  43580  hoicvr  43976  ovolval3  44075