Theorem fdmi 6743

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

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5655  ⟶wf 6554

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 402  df-fn 6561  df-f 6562

This theorem is used by:  f0cli  7122  rankvaln  9834  isnum2  10053  r0weon  10118  cfub  10353  cardcf  10356  cflecard  10357  cfle  10358  cflim2  10368  cfidm  10380  cardf  10661  smobeth  10698  inar1  10887  addcompq  11062  addcomnq  11063  mulcompq  11064  mulcomnq  11065  adderpq  11068  mulerpq  11069  addassnq  11070  mulassnq  11071  distrnq  11073  recmulnq  11076  recclnq  11078  dmrecnq  11080  lterpq  11082  ltanq  11083  ltmnq  11084  ltexnq  11087  nsmallnq  11089  ltbtwnnq  11090  prlem934  11145  ltaddpr  11146  ltexprlem2  11149  ltexprlem3  11150  ltexprlem4  11151  ltexprlem6  11153  ltexprlem7  11154  prlem936  11159  eluzel2  12997  uzssz  13013  elixx3g  13516  ndmioo  13530  elfz2  13673  fz0  13699  elfzoel1  13818  elfzoel2  13819  fzoval  13821  ltweuz  14131  fzofi  14144  dmhashres  14512  s1dm  14782  s2dm  15069  sumz  15917  sumss  15919  prod1  16140  prodss  16143  znnen  16409  unbenlem  17115  prmreclem6  17128  eldmcoa  18269  efgsdm  19974  efgsval  19975  efgsp1  19981  efgsfo  19983  efgredleme  19987  efgred  19992  gexex  20097  torsubg  20098  dmdprd  20244  dprdval  20249  iocpnfordt  23563  icomnfordt  23564  uzrest  24246  qtopbaslem  25107  retopbas  25109  tgqioo  25149  re2ndc  25150  bndth  25309  tcphcph  25588  ovolficcss  25820  ismbl  25877  uniiccdif  25929  dyadmbllem  25950  opnmbllem  25952  opnmblALT  25954  mbfimaopnlem  26006  itg1addlem4  26050  dvcmul  26294  dvcmulf  26295  dvexp  26303  c1liplem1  26346  deg1n0ima  26437  pserulm  26779  psercn2  26780  psercnlem2  26781  psercnlem1  26782  psercn  26783  pserdvlem1  26784  pserdvlem2  26785  pserdv  26786  pserdv2  26787  abelth  26798  efcn  26800  efcvx  26806  eff1olem  26906  dvrelog  26995  logf1o2  27008  dvlog  27009  efopn  27016  logtayl  27018  cxpcn3lem  27105  cxpcn3  27106  resqrtcn  27107  atancl  27239  atanval  27242  dvatan  27293  atancn  27294  bdaydmOLD  28166  lltr  28278  madess  28282  oldssmade  28283  oldss  28286  madebdayim  28304  oldbdayim  28305  lrold  28313  madefi  28329  oldfi  28330  cutminmax  28352  oldfib  28793  topnfbey  31100  cnaddabloOLD  31213  cnidOLD  31214  cncvcOLD  31215  cnnv  31309  cnnvba  31311  cncph  31451  dfhnorm2  31754  hilablo  31792  hilid  31793  hilvc  31794  hhnv  31797  hhba  31799  hhph  31810  issh2  31841  hhssabloi  31894  hhssnv  31896  hhshsslem1  31899  imaelshi  32690  rnelshi  32691  nlelshi  32692  xrofsup  33429  ply1degltel  34196  ply1degleel  34197  ply1degltlss  34198  coinfliprv  35185  dfscott3  35827  j00smo  36005  erdszelem2  36124  erdszelem5  36127  erdszelem8  36130  msrrcl  36475  mthmsta  36510  icoreunrn  38474  icoreelrn  38476  relowlpssretop  38479  poimirlem26  38756  poimirlem27  38757  opnmbllem0  38766  dvtan  38780  fpwfvss  44605  seff  45485  sblpnf  45486  dvsconst  45506  dvsid  45507  dvsef  45508  expgrowth  45511  binomcxplemdvbinom  45529  binomcxplemdvsum  45531  binomcxplemnotnn0  45532  addcomgi  45629  dmuz  46451  dmico  46780  dvsinax  47128  fvvolioof  47204  fvvolicof  47206  dirkercncflem2  47319  fourierdlem42  47364  hoicvr  47763  ovolval3  47862  tannpoly  48145  sinnpoly  48146  fucofvalne  50652  dvsec  51136  dvcsc  51137  dvcot  51138