Theorem fdmi 6699

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

Syntax hints:   = wceq 1540  dom cdm 5638  ⟶wf 6507

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 207  df-an 396  df-fn 6514  df-f 6515

This theorem is referenced by:  f0cli  7070  rankvaln  9752  isnum2  9898  r0weon  9965  cfub  10202  cardcf  10205  cflecard  10206  cfle  10207  cflim2  10216  cfidm  10228  cardf  10503  smobeth  10539  inar1  10728  addcompq  10903  addcomnq  10904  mulcompq  10905  mulcomnq  10906  adderpq  10909  mulerpq  10910  addassnq  10911  mulassnq  10912  distrnq  10914  recmulnq  10917  recclnq  10919  dmrecnq  10921  lterpq  10923  ltanq  10924  ltmnq  10925  ltexnq  10928  nsmallnq  10930  ltbtwnnq  10931  prlem934  10986  ltaddpr  10987  ltexprlem2  10990  ltexprlem3  10991  ltexprlem4  10992  ltexprlem6  10994  ltexprlem7  10995  prlem936  11000  eluzel2  12798  uzssz  12814  elixx3g  13319  ndmioo  13333  elfz2  13475  fz0  13500  elfzoel1  13618  elfzoel2  13619  fzoval  13621  ltweuz  13926  fzofi  13939  dmhashres  14306  s1dm  14573  s2dm  14856  sumz  15688  sumss  15690  prod1  15910  prodss  15913  znnen  16180  unbenlem  16879  prmreclem6  16892  eldmcoa  18027  efgsdm  19660  efgsval  19661  efgsp1  19667  efgsfo  19669  efgredleme  19673  efgred  19678  gexex  19783  torsubg  19784  dmdprd  19930  dprdval  19935  iocpnfordt  23102  icomnfordt  23103  uzrest  23784  qtopbaslem  24646  retopbas  24648  tgqioo  24688  re2ndc  24689  bndth  24857  tcphcph  25137  ovolficcss  25370  ismbl  25427  uniiccdif  25479  dyadmbllem  25500  opnmbllem  25502  opnmblALT  25504  mbfimaopnlem  25556  itg1addlem4  25600  dvcmul  25847  dvcmulf  25848  dvexp  25857  c1liplem1  25901  deg1n0ima  25994  pserulm  26331  psercn2  26332  psercn2OLD  26333  psercnlem2  26334  psercnlem1  26335  psercn  26336  pserdvlem1  26337  pserdvlem2  26338  pserdv  26339  pserdv2  26340  abelth  26351  efcn  26353  efcvx  26359  eff1olem  26457  dvrelog  26546  logf1o2  26559  dvlog  26560  efopn  26567  logtayl  26569  cxpcn3lem  26657  cxpcn3  26658  resqrtcn  26659  atancl  26791  atanval  26794  dvatan  26845  atancn  26846  bdaydm  27686  lltropt  27784  madess  27788  oldssmade  27789  madebdayim  27799  oldbdayim  27800  lrold  27808  madefi  27824  oldfi  27825  topnfbey  30398  cnaddabloOLD  30510  cnidOLD  30511  cncvcOLD  30512  cnnv  30606  cnnvba  30608  cncph  30748  dfhnorm2  31051  hilablo  31089  hilid  31090  hilvc  31091  hhnv  31094  hhba  31096  hhph  31107  issh2  31138  hhssabloi  31191  hhssnv  31193  hhshsslem1  31196  imaelshi  31987  rnelshi  31988  nlelshi  31989  xrofsup  32690  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  coinfliprv  34474  erdszelem2  35179  erdszelem5  35182  erdszelem8  35185  msrrcl  35530  mthmsta  35565  icoreunrn  37347  icoreelrn  37349  relowlpssretop  37352  poimirlem26  37640  poimirlem27  37641  opnmbllem0  37650  dvtan  37664  fpwfvss  43401  seff  44298  sblpnf  44299  dvsconst  44319  dvsid  44320  dvsef  44321  expgrowth  44324  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  addcomgi  44445  dmuz  45228  dmico  45561  dvsinax  45911  fvvolioof  45987  fvvolicof  45989  dirkercncflem2  46102  fourierdlem42  46147  hoicvr  46546  ovolval3  46645  sinnpoly  46892  fucofvalne  49314