Theorem fdmi 6717

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

This proof depends on syntax axioms:   = wceq 1569  dom cdm 5660  ⟶wf 6532

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 401  df-fn 6539  df-f 6540

This theorem is used by:  f0cli  7093  rankvaln  9769  isnum2  9938  r0weon  10003  cfub  10238  cardcf  10241  cflecard  10242  cfle  10243  cflim2  10253  cfidm  10265  cardf  10540  smobeth  10577  inar1  10766  addcompq  10941  addcomnq  10942  mulcompq  10943  mulcomnq  10944  adderpq  10947  mulerpq  10948  addassnq  10949  mulassnq  10950  distrnq  10952  recmulnq  10955  recclnq  10957  dmrecnq  10959  lterpq  10961  ltanq  10962  ltmnq  10963  ltexnq  10966  nsmallnq  10968  ltbtwnnq  10969  prlem934  11024  ltaddpr  11025  ltexprlem2  11028  ltexprlem3  11029  ltexprlem4  11030  ltexprlem6  11032  ltexprlem7  11033  prlem936  11038  eluzel2  12873  uzssz  12889  elixx3g  13391  ndmioo  13405  elfz2  13548  fz0  13573  elfzoel1  13692  elfzoel2  13693  fzoval  13695  ltweuz  14004  fzofi  14017  dmhashres  14384  s1dm  14653  s2dm  14934  sumz  15780  sumss  15782  prod1  16005  prodss  16008  znnen  16274  unbenlem  16974  prmreclem6  16987  eldmcoa  18128  efgsdm  19806  efgsval  19807  efgsp1  19813  efgsfo  19815  efgredleme  19819  efgred  19824  gexex  19929  torsubg  19930  dmdprd  20076  dprdval  20081  iocpnfordt  23383  icomnfordt  23384  uzrest  24065  qtopbaslem  24926  retopbas  24928  tgqioo  24968  re2ndc  24969  bndth  25128  tcphcph  25407  ovolficcss  25639  ismbl  25696  uniiccdif  25748  dyadmbllem  25769  opnmbllem  25771  opnmblALT  25773  mbfimaopnlem  25825  itg1addlem4  25869  dvcmul  26114  dvcmulf  26115  dvexp  26123  c1liplem1  26166  deg1n0ima  26257  pserulm  26596  psercn2  26597  psercnlem2  26598  psercnlem1  26599  psercn  26600  pserdvlem1  26601  pserdvlem2  26602  pserdv  26603  pserdv2  26604  abelth  26615  efcn  26617  efcvx  26623  eff1olem  26724  dvrelog  26813  logf1o2  26826  dvlog  26827  efopn  26834  logtayl  26836  cxpcn3lem  26923  cxpcn3  26924  resqrtcn  26925  atancl  27057  atanval  27060  dvatan  27111  atancn  27112  bdaydmOLD  27954  lltr  28066  madess  28070  oldssmade  28071  oldss  28074  madebdayim  28092  oldbdayim  28093  lrold  28101  madefi  28117  oldfi  28118  cutminmax  28140  oldfib  28581  topnfbey  30831  cnaddabloOLD  30944  cnidOLD  30945  cncvcOLD  30946  cnnv  31040  cnnvba  31042  cncph  31182  dfhnorm2  31485  hilablo  31523  hilid  31524  hilvc  31525  hhnv  31528  hhba  31530  hhph  31541  issh2  31572  hhssabloi  31625  hhssnv  31627  hhshsslem1  31630  imaelshi  32421  rnelshi  32422  nlelshi  32423  xrofsup  33123  ply1degltel  33893  ply1degleel  33894  ply1degltlss  33895  coinfliprv  34882  dfscott3  35521  erdszelem2  35692  erdszelem5  35695  erdszelem8  35698  msrrcl  36043  mthmsta  36078  icoreunrn  38033  icoreelrn  38035  relowlpssretop  38038  poimirlem26  38325  poimirlem27  38326  opnmbllem0  38335  dvtan  38349  fpwfvss  44166  seff  45047  sblpnf  45048  dvsconst  45068  dvsid  45069  dvsef  45070  expgrowth  45073  binomcxplemdvbinom  45091  binomcxplemdvsum  45093  binomcxplemnotnn0  45094  addcomgi  45192  dmuz  45977  dmico  46307  dvsinax  46655  fvvolioof  46731  fvvolicof  46733  dirkercncflem2  46846  fourierdlem42  46891  hoicvr  47290  ovolval3  47389  sinnpoly  47656  fucofvalne  50131