Theorem fdmi 6673

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

Syntax hints:   = wceq 1547  dom cdm 5625  ⟶wf 6488

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 208  df-an 397  df-fn 6495  df-f 6496

This theorem is referenced by:  f0cli  7046  rankvaln  9721  isnum2  9867  r0weon  9932  cfub  10169  cardcf  10172  cflecard  10173  cfle  10174  cflim2  10183  cfidm  10195  cardf  10470  smobeth  10507  inar1  10696  addcompq  10871  addcomnq  10872  mulcompq  10873  mulcomnq  10874  adderpq  10877  mulerpq  10878  addassnq  10879  mulassnq  10880  distrnq  10882  recmulnq  10885  recclnq  10887  dmrecnq  10889  lterpq  10891  ltanq  10892  ltmnq  10893  ltexnq  10896  nsmallnq  10898  ltbtwnnq  10899  prlem934  10954  ltaddpr  10955  ltexprlem2  10958  ltexprlem3  10959  ltexprlem4  10960  ltexprlem6  10962  ltexprlem7  10963  prlem936  10968  eluzel2  12791  uzssz  12807  elixx3g  13309  ndmioo  13323  elfz2  13466  fz0  13491  elfzoel1  13609  elfzoel2  13610  fzoval  13612  ltweuz  13921  fzofi  13934  dmhashres  14301  s1dm  14569  s2dm  14850  sumz  15682  sumss  15684  prod1  15907  prodss  15910  znnen  16177  unbenlem  16877  prmreclem6  16890  eldmcoa  18030  efgsdm  19703  efgsval  19704  efgsp1  19710  efgsfo  19712  efgredleme  19716  efgred  19721  gexex  19826  torsubg  19827  dmdprd  19973  dprdval  19978  iocpnfordt  23205  icomnfordt  23206  uzrest  23887  qtopbaslem  24748  retopbas  24750  tgqioo  24790  re2ndc  24791  bndth  24950  tcphcph  25229  ovolficcss  25461  ismbl  25518  uniiccdif  25570  dyadmbllem  25591  opnmbllem  25593  opnmblALT  25595  mbfimaopnlem  25647  itg1addlem4  25691  dvcmul  25936  dvcmulf  25937  dvexp  25945  c1liplem1  25988  deg1n0ima  26079  pserulm  26412  psercn2  26413  psercnlem2  26414  psercnlem1  26415  psercn  26416  pserdvlem1  26417  pserdvlem2  26418  pserdv  26419  pserdv2  26420  abelth  26431  efcn  26433  efcvx  26439  eff1olem  26537  dvrelog  26626  logf1o2  26639  dvlog  26640  efopn  26647  logtayl  26649  cxpcn3lem  26736  cxpcn3  26737  resqrtcn  26738  atancl  26870  atanval  26873  dvatan  26924  atancn  26925  bdaydm  27767  lltr  27879  madess  27883  oldssmade  27884  oldss  27887  madebdayim  27905  oldbdayim  27906  lrold  27914  madefi  27930  oldfi  27931  cutminmax  27953  oldfib  28394  topnfbey  30564  cnaddabloOLD  30677  cnidOLD  30678  cncvcOLD  30679  cnnv  30773  cnnvba  30775  cncph  30915  dfhnorm2  31218  hilablo  31256  hilid  31257  hilvc  31258  hhnv  31261  hhba  31263  hhph  31274  issh2  31305  hhssabloi  31358  hhssnv  31360  hhshsslem1  31363  imaelshi  32154  rnelshi  32155  nlelshi  32156  xrofsup  32866  ply1degltel  33684  ply1degleel  33685  ply1degltlss  33686  coinfliprv  34674  erdszelem2  35421  erdszelem5  35424  erdszelem8  35427  msrrcl  35772  mthmsta  35807  icoreunrn  37722  icoreelrn  37724  relowlpssretop  37727  poimirlem26  38014  poimirlem27  38015  opnmbllem0  38024  dvtan  38038  fpwfvss  43857  seff  44754  sblpnf  44755  dvsconst  44775  dvsid  44776  dvsef  44777  expgrowth  44780  binomcxplemdvbinom  44798  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  addcomgi  44900  dmuz  45679  dmico  46009  dvsinax  46357  fvvolioof  46433  fvvolicof  46435  dirkercncflem2  46548  fourierdlem42  46593  hoicvr  46992  ovolval3  47091  sinnpoly  47355  fucofvalne  49816