Theorem fndmd 6538

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 6536	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5589   Fn wfn 6428

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 6436

This theorem is referenced by:  fdm  6609  f1dm  6674  f1o00  6751  fvelimad  6836  rescnvimafod  6951  f1eqcocnv  7173  ofrfvalg  7541  offval  7542  fndmexd  7753  dmmpoga  7913  fnwelem  7972  frrlem4  8105  frrlem8  8109  frrlem10  8111  fpr2  8120  fprresex  8126  wfrlem17OLD  8156  wfr2  8167  tfrlem5  8211  ixpiunwdom  9349  frr2  9518  dfac12lem1  9899  ackbij2lem3  9997  itunisuc  10175  ttukeylem3  10267  prdsbas2  17180  prdsplusgval  17184  prdsmulrval  17186  prdsleval  17188  prdsvscaval  17190  imasleval  17252  ssclem  17531  isssc  17532  rescval2  17540  issubc2  17551  cofuval  17597  resfval2  17608  resf1st  17609  resf2nd  17610  prdsmgp  19849  lspextmo  20318  dsmmfi  20945  ofco2  21600  neiss2  22252  txdis1cn  22786  qtopcld  22864  qtoprest  22868  kqsat  22882  kqdisj  22883  isr0  22888  elfm3  23101  ovolunlem1  24661  ofpreima  31002  ofpreima2  31003  fnpreimac  31008  fsuppcurry1  31060  fsuppcurry2  31061  pfxf1  31216  s2rn  31218  s3rn  31220  cycpmfvlem  31379  cycpmfv1  31380  cycpmfv2  31381  cycpmfv3  31382  ofcfval  32066  probfinmeasb  32395  bnj564  32724  bnj1121  32965  bnj1442  33029  bnj1450  33030  bnj1501  33047  fnrelpredd  33061  sdclem2  35900  prdstotbnd  35952  diadm  39049  dibdiadm  39169  dibdmN  39171  dicdmN  39198  dihdm  39283  aks4d1p1p5  40083  fnchoice  42572  wessf1ornlem  42722  limsupequzlem  43263  climrescn  43289  icccncfext  43428  stoweidlem35  43576  stoweidlem59  43600  smflimmpt  44343  smflimsuplem7  44359