Theorem fdmi 6734

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

Syntax hints:   = wceq 1533  dom cdm 5678  ⟶wf 6545

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 395  df-fn 6552  df-f 6553

This theorem is referenced by:  f0cli  7107  rankvaln  9824  isnum2  9970  r0weon  10037  cfub  10274  cardcf  10277  cflecard  10278  cfle  10279  cflim2  10288  cfidm  10300  cardf  10575  smobeth  10611  inar1  10800  addcompq  10975  addcomnq  10976  mulcompq  10977  mulcomnq  10978  adderpq  10981  mulerpq  10982  addassnq  10983  mulassnq  10984  distrnq  10986  recmulnq  10989  recclnq  10991  dmrecnq  10993  lterpq  10995  ltanq  10996  ltmnq  10997  ltexnq  11000  nsmallnq  11002  ltbtwnnq  11003  prlem934  11058  ltaddpr  11059  ltexprlem2  11062  ltexprlem3  11063  ltexprlem4  11064  ltexprlem6  11066  ltexprlem7  11067  prlem936  11072  eluzel2  12860  uzssz  12876  elixx3g  13372  ndmioo  13386  elfz2  13526  fz0  13551  elfzoel1  13665  elfzoel2  13666  fzoval  13668  ltweuz  13962  fzofi  13975  dmhashres  14336  s1dm  14594  s2dm  14877  sumz  15704  sumss  15706  prod1  15924  prodss  15927  znnen  16192  unbenlem  16880  prmreclem6  16893  eldmcoa  18057  efgsdm  19697  efgsval  19698  efgsp1  19704  efgsfo  19706  efgredleme  19710  efgred  19715  gexex  19820  torsubg  19821  dmdprd  19967  dprdval  19972  iocpnfordt  23163  icomnfordt  23164  uzrest  23845  qtopbaslem  24719  retopbas  24721  tgqioo  24760  re2ndc  24761  bndth  24928  tcphcph  25209  ovolficcss  25442  ismbl  25499  uniiccdif  25551  dyadmbllem  25572  opnmbllem  25574  opnmblALT  25576  mbfimaopnlem  25628  itg1addlem4  25672  itg1addlem4OLD  25673  dvcmul  25919  dvcmulf  25920  dvexp  25929  c1liplem1  25973  deg1n0ima  26069  pserulm  26403  psercn2  26404  psercn2OLD  26405  psercnlem2  26406  psercnlem1  26407  psercn  26408  pserdvlem1  26409  pserdvlem2  26410  pserdv  26411  pserdv2  26412  abelth  26423  efcn  26425  efcvx  26431  eff1olem  26527  dvrelog  26616  logf1o2  26629  dvlog  26630  efopn  26637  logtayl  26639  cxpcn3lem  26727  cxpcn3  26728  resqrtcn  26729  atancl  26858  atanval  26861  dvatan  26912  atancn  26913  bdaydm  27753  lltropt  27845  madess  27849  oldssmade  27850  madebdayim  27860  oldbdayim  27861  lrold  27869  topnfbey  30351  cnaddabloOLD  30463  cnidOLD  30464  cncvcOLD  30465  cnnv  30559  cnnvba  30561  cncph  30701  dfhnorm2  31004  hilablo  31042  hilid  31043  hilvc  31044  hhnv  31047  hhba  31049  hhph  31060  issh2  31091  hhssabloi  31144  hhssnv  31146  hhshsslem1  31149  imaelshi  31940  rnelshi  31941  nlelshi  31942  xrofsup  32619  ply1degltel  33396  ply1degleel  33397  ply1degltlss  33398  coinfliprv  34233  erdszelem2  34933  erdszelem5  34936  erdszelem8  34939  msrrcl  35284  mthmsta  35319  icoreunrn  36969  icoreelrn  36971  relowlpssretop  36974  poimirlem26  37250  poimirlem27  37251  opnmbllem0  37260  dvtan  37274  fpwfvss  42984  seff  43888  sblpnf  43889  dvsconst  43909  dvsid  43910  dvsef  43911  expgrowth  43914  binomcxplemdvbinom  43932  binomcxplemdvsum  43934  binomcxplemnotnn0  43935  addcomgi  44035  dmuz  44746  dmico  45088  dvsinax  45439  fvvolioof  45515  fvvolicof  45517  dirkercncflem2  45630  fourierdlem42  45675  hoicvr  46074  ovolval3  46173