Theorem fdmi 6658

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

Syntax hints:   = wceq 1541  dom cdm 5614  ⟶wf 6473

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 6480  df-f 6481

This theorem is referenced by:  f0cli  7026  rankvaln  9684  isnum2  9830  r0weon  9895  cfub  10132  cardcf  10135  cflecard  10136  cfle  10137  cflim2  10146  cfidm  10158  cardf  10433  smobeth  10469  inar1  10658  addcompq  10833  addcomnq  10834  mulcompq  10835  mulcomnq  10836  adderpq  10839  mulerpq  10840  addassnq  10841  mulassnq  10842  distrnq  10844  recmulnq  10847  recclnq  10849  dmrecnq  10851  lterpq  10853  ltanq  10854  ltmnq  10855  ltexnq  10858  nsmallnq  10860  ltbtwnnq  10861  prlem934  10916  ltaddpr  10917  ltexprlem2  10920  ltexprlem3  10921  ltexprlem4  10922  ltexprlem6  10924  ltexprlem7  10925  prlem936  10930  eluzel2  12729  uzssz  12745  elixx3g  13250  ndmioo  13264  elfz2  13406  fz0  13431  elfzoel1  13549  elfzoel2  13550  fzoval  13552  ltweuz  13860  fzofi  13873  dmhashres  14240  s1dm  14508  s2dm  14789  sumz  15621  sumss  15623  prod1  15843  prodss  15846  znnen  16113  unbenlem  16812  prmreclem6  16825  eldmcoa  17964  efgsdm  19635  efgsval  19636  efgsp1  19642  efgsfo  19644  efgredleme  19648  efgred  19653  gexex  19758  torsubg  19759  dmdprd  19905  dprdval  19910  iocpnfordt  23123  icomnfordt  23124  uzrest  23805  qtopbaslem  24666  retopbas  24668  tgqioo  24708  re2ndc  24709  bndth  24877  tcphcph  25157  ovolficcss  25390  ismbl  25447  uniiccdif  25499  dyadmbllem  25520  opnmbllem  25522  opnmblALT  25524  mbfimaopnlem  25576  itg1addlem4  25620  dvcmul  25867  dvcmulf  25868  dvexp  25877  c1liplem1  25921  deg1n0ima  26014  pserulm  26351  psercn2  26352  psercn2OLD  26353  psercnlem2  26354  psercnlem1  26355  psercn  26356  pserdvlem1  26357  pserdvlem2  26358  pserdv  26359  pserdv2  26360  abelth  26371  efcn  26373  efcvx  26379  eff1olem  26477  dvrelog  26566  logf1o2  26579  dvlog  26580  efopn  26587  logtayl  26589  cxpcn3lem  26677  cxpcn3  26678  resqrtcn  26679  atancl  26811  atanval  26814  dvatan  26865  atancn  26866  bdaydm  27706  lltropt  27810  madess  27814  oldssmade  27815  oldss  27816  madebdayim  27826  oldbdayim  27827  lrold  27835  madefi  27851  oldfi  27852  topnfbey  30439  cnaddabloOLD  30551  cnidOLD  30552  cncvcOLD  30553  cnnv  30647  cnnvba  30649  cncph  30789  dfhnorm2  31092  hilablo  31130  hilid  31131  hilvc  31132  hhnv  31135  hhba  31137  hhph  31148  issh2  31179  hhssabloi  31232  hhssnv  31234  hhshsslem1  31237  imaelshi  32028  rnelshi  32029  nlelshi  32030  xrofsup  32740  ply1degltel  33545  ply1degleel  33546  ply1degltlss  33547  coinfliprv  34486  erdszelem2  35204  erdszelem5  35207  erdszelem8  35210  msrrcl  35555  mthmsta  35590  icoreunrn  37372  icoreelrn  37374  relowlpssretop  37377  poimirlem26  37665  poimirlem27  37666  opnmbllem0  37675  dvtan  37689  fpwfvss  43424  seff  44321  sblpnf  44322  dvsconst  44342  dvsid  44343  dvsef  44344  expgrowth  44347  binomcxplemdvbinom  44365  binomcxplemdvsum  44367  binomcxplemnotnn0  44368  addcomgi  44467  dmuz  45250  dmico  45582  dvsinax  45930  fvvolioof  46006  fvvolicof  46008  dirkercncflem2  46121  fourierdlem42  46166  hoicvr  46565  ovolval3  46664  sinnpoly  46901  fucofvalne  49336