Theorem fndmd 6591

Description: The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
fndmd.1	⊢ (𝜑 → 𝐹 Fn 𝐴)

Assertion

Ref	Expression
fndmd	⊢ (𝜑 → dom 𝐹 = 𝐴)

Proof of Theorem fndmd

Step	Hyp	Ref	Expression
1		fndmd.1	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
2		fndm 6589	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5619   Fn wfn 6481

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 6489

This theorem is referenced by:  fdm  6665  f1dm  6728  f1o00  6803  fvelimad  6895  rescnvimafod  7012  f1eqcocnv  7241  ofrfvalg  7624  offval  7625  fndmexd  7840  dmmpoga  8011  fnwelem  8067  frrlem4  8225  frrlem8  8229  frrlem10  8231  fpr2  8240  fprresex  8246  wfr2  8263  tfrlem5  8305  ixpiunwdom  9483  frr2  9660  dfac12lem1  10042  ackbij2lem3  10138  itunisuc  10317  ttukeylem3  10409  prdsbas2  17375  prdsplusgval  17379  prdsmulrval  17381  prdsleval  17383  prdsvscaval  17385  imasleval  17447  ssclem  17728  isssc  17729  rescval2  17737  issubc2  17745  cofuval  17791  resfval2  17802  resf1st  17803  resf2nd  17804  prdsmgp  20071  lspextmo  20992  dsmmfi  21677  ofco2  22367  neiss2  23017  txdis1cn  23551  qtopcld  23629  qtoprest  23633  kqsat  23647  kqdisj  23648  isr0  23653  elfm3  23866  ovolunlem1  25426  ofpreima  32649  ofpreima2  32650  fnpreimac  32655  fsuppcurry1  32711  fsuppcurry2  32712  pfxf1  32930  s2rnOLD  32932  s3rnOLD  32934  cycpmfvlem  33088  cycpmfv1  33089  cycpmfv2  33090  cycpmfv3  33091  1arithidomlem2  33508  1arithidom  33509  esplyind  33613  ply1annidllem  33735  ofcfval  34132  probfinmeasb  34462  bnj564  34777  bnj1121  35018  bnj1442  35082  bnj1450  35083  bnj1501  35100  fnrelpredd  35123  sdclem2  37802  prdstotbnd  37854  diadm  41154  dibdiadm  41274  dibdmN  41276  dicdmN  41303  dihdm  41388  aks4d1p1p5  42188  aks6d1c6lem2  42284  tfsconcat0b  43463  fnchoice  45150  wessf1ornlem  45306  limsupequzlem  45844  climrescn  45870  icccncfext  46009  stoweidlem35  46157  stoweidlem59  46181  smflimmpt  46932  smflimsuplem7  46948  iinfssclem1  49179  infsubc2d  49187  oppfvallem  49260  funcoppc3  49272  uptposlem  49322