Theorem fdmi 6729

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

Syntax hints:   = wceq 1541  dom cdm 5676  ⟶wf 6539

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 397  df-fn 6546  df-f 6547

This theorem is referenced by:  f0cli  7099  rankvaln  9796  isnum2  9942  r0weon  10009  cfub  10246  cardcf  10249  cflecard  10250  cfle  10251  cflim2  10260  cfidm  10272  cardf  10547  smobeth  10583  inar1  10772  addcompq  10947  addcomnq  10948  mulcompq  10949  mulcomnq  10950  adderpq  10953  mulerpq  10954  addassnq  10955  mulassnq  10956  distrnq  10958  recmulnq  10961  recclnq  10963  dmrecnq  10965  lterpq  10967  ltanq  10968  ltmnq  10969  ltexnq  10972  nsmallnq  10974  ltbtwnnq  10975  prlem934  11030  ltaddpr  11031  ltexprlem2  11034  ltexprlem3  11035  ltexprlem4  11036  ltexprlem6  11038  ltexprlem7  11039  prlem936  11044  eluzel2  12829  uzssz  12845  elixx3g  13339  ndmioo  13353  elfz2  13493  fz0  13518  elfzoel1  13632  elfzoel2  13633  fzoval  13635  ltweuz  13928  fzofi  13941  dmhashres  14303  s1dm  14560  s2dm  14843  sumz  15670  sumss  15672  prod1  15890  prodss  15893  znnen  16157  unbenlem  16843  prmreclem6  16856  eldmcoa  18017  efgsdm  19600  efgsval  19601  efgsp1  19607  efgsfo  19609  efgredleme  19613  efgred  19618  gexex  19723  torsubg  19724  dmdprd  19870  dprdval  19875  iocpnfordt  22726  icomnfordt  22727  uzrest  23408  qtopbaslem  24282  retopbas  24284  tgqioo  24323  re2ndc  24324  bndth  24481  tcphcph  24761  ovolficcss  24993  ismbl  25050  uniiccdif  25102  dyadmbllem  25123  opnmbllem  25125  opnmblALT  25127  mbfimaopnlem  25179  itg1addlem4  25223  itg1addlem4OLD  25224  dvcmul  25468  dvcmulf  25469  dvexp  25477  c1liplem1  25520  deg1n0ima  25614  pserulm  25941  psercn2  25942  psercnlem2  25943  psercnlem1  25944  psercn  25945  pserdvlem1  25946  pserdvlem2  25947  pserdv  25948  pserdv2  25949  abelth  25960  efcn  25962  efcvx  25968  eff1olem  26064  dvrelog  26152  logf1o2  26165  dvlog  26166  efopn  26173  logtayl  26175  cxpcn3lem  26262  cxpcn3  26263  resqrtcn  26264  atancl  26393  atanval  26396  dvatan  26447  atancn  26448  bdaydm  27283  lltropt  27375  madess  27379  oldssmade  27380  madebdayim  27390  oldbdayim  27391  lrold  27399  topnfbey  29760  cnaddabloOLD  29872  cnidOLD  29873  cncvcOLD  29874  cnnv  29968  cnnvba  29970  cncph  30110  dfhnorm2  30413  hilablo  30451  hilid  30452  hilvc  30453  hhnv  30456  hhba  30458  hhph  30469  issh2  30500  hhssabloi  30553  hhssnv  30555  hhshsslem1  30558  imaelshi  31349  rnelshi  31350  nlelshi  31351  xrofsup  32018  ply1degltel  32711  ply1degleel  32712  ply1degltlss  32713  coinfliprv  33550  erdszelem2  34252  erdszelem5  34255  erdszelem8  34258  msrrcl  34603  mthmsta  34638  gg-psercn2  35253  icoreunrn  36332  icoreelrn  36334  relowlpssretop  36337  poimirlem26  36606  poimirlem27  36607  opnmbllem0  36616  dvtan  36630  fpwfvss  42251  seff  43156  sblpnf  43157  dvsconst  43177  dvsid  43178  dvsef  43179  expgrowth  43182  binomcxplemdvbinom  43200  binomcxplemdvsum  43202  binomcxplemnotnn0  43203  addcomgi  43303  dmuz  44021  dmico  44363  dvsinax  44714  fvvolioof  44790  fvvolicof  44792  dirkercncflem2  44905  fourierdlem42  44950  hoicvr  45349  ovolval3  45448