Theorem fndmd 6653

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

Syntax hints:   → wi 4   = wceq 1534  dom cdm 5672   Fn wfn 6537

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 396  df-fn 6545

This theorem is referenced by:  fdm  6725  f1dm  6791  f1o00  6868  fvelimad  6960  rescnvimafod  7077  f1eqcocnv  7304  ofrfvalg  7687  offval  7688  fndmexd  7906  dmmpoga  8071  fnwelem  8130  frrlem4  8288  frrlem8  8292  frrlem10  8294  fpr2  8303  fprresex  8309  wfrlem17OLD  8339  wfr2  8350  tfrlem5  8394  ixpiunwdom  9605  frr2  9775  dfac12lem1  10158  ackbij2lem3  10256  itunisuc  10434  ttukeylem3  10526  prdsbas2  17442  prdsplusgval  17446  prdsmulrval  17448  prdsleval  17450  prdsvscaval  17452  imasleval  17514  ssclem  17793  isssc  17794  rescval2  17802  issubc2  17813  cofuval  17859  resfval2  17870  resf1st  17871  resf2nd  17872  prdsmgp  20082  lspextmo  20930  dsmmfi  21659  ofco2  22340  neiss2  22992  txdis1cn  23526  qtopcld  23604  qtoprest  23608  kqsat  23622  kqdisj  23623  isr0  23628  elfm3  23841  ovolunlem1  25413  ofpreima  32434  ofpreima2  32435  fnpreimac  32440  fsuppcurry1  32491  fsuppcurry2  32492  pfxf1  32647  s2rn  32649  s3rn  32651  cycpmfvlem  32811  cycpmfv1  32812  cycpmfv2  32813  cycpmfv3  32814  ply1annidllem  33308  ofcfval  33653  probfinmeasb  33984  bnj564  34311  bnj1121  34552  bnj1442  34616  bnj1450  34617  bnj1501  34634  fnrelpredd  34648  sdclem2  37150  prdstotbnd  37202  diadm  40445  dibdiadm  40565  dibdmN  40567  dicdmN  40594  dihdm  40679  aks4d1p1p5  41483  aks6d1c6lem2  41575  tfsconcat0b  42698  fnchoice  44314  wessf1ornlem  44481  limsupequzlem  45033  climrescn  45059  icccncfext  45198  stoweidlem35  45346  stoweidlem59  45370  smflimmpt  46121  smflimsuplem7  46137